Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem 19.43 1086

Description: Theorem 19.43 of [Margaris] p. 90.

Assertion

Ref	Expression
19.43

---

Proof of Theorem 19.43

Step	Hyp	Ref	Expression
1		ioran 306	. . . . 5
2	1	albii 997	. . . 4
3		19.26 1065	. . . 4
4		alnex 1031	. . . . 5
5		alnex 1031	. . . . 5
6	4, 5	anbi12i 482	. . . 4
7	2, 3, 6	3bitr 177	. . 3
8	7	negbii 187	. 2
9		df-ex 979	. 2
10		oran 312	. 2
11	8, 9, 10	3bitr4 183	1

Colors of variables: wff set class

Syntax hints:   wn 2   wb 146   wo 222   wa 223  wal 952  wex 978

This theorem is referenced by:  19.44 1087  19.45 1088  19.34 1091  euor2 1435  r19.43 1762  unipr 2510  uniun 2514  iunxun 2609  unopab 2674  zfpair 2772  dmun 3312  oarec 4186  kmlem16 4760

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-4 971  ax-5o 973

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979

Copyright terms: Public domain