Mathbox for Jonathan Ben-Naim < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj1304 Structured version   Unicode version

Theorem bnj1304 29118
 Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Hypotheses
Ref Expression
bnj1304.1
bnj1304.2
bnj1304.3
Assertion
Ref Expression
bnj1304

Proof of Theorem bnj1304
StepHypRef Expression
1 notnot 283 . . . 4
2 notnot 283 . . . . . . . 8
32anbi2i 676 . . . . . . 7
43exbii 1592 . . . . . 6
5 ioran 477 . . . . . . 7
65exbii 1592 . . . . . 6
7 exnal 1583 . . . . . 6
84, 6, 73bitr2ri 266 . . . . 5
98notbii 288 . . . 4
10 exancom 1596 . . . . 5
1110notbii 288 . . . 4
121, 9, 113bitri 263 . . 3
13 exmid 405 . . 3
1412, 13mpgbi 1558 . 2
15 bnj1304.1 . . 3
16 bnj1304.2 . . . 4
17 bnj1304.3 . . . 4
1816, 17jca 519 . . 3
1915, 18bnj593 29040 . 2
2014, 19mto 169 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wo 358   wa 359  wal 1549  wex 1550 This theorem is referenced by:  bnj1204  29308  bnj1279  29314  bnj1311  29320  bnj1312  29354 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-ex 1551
 Copyright terms: Public domain W3C validator