Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  19.26 Unicode version

Theorem 19.26 1458
 Description: Theorem 19.26 of [Margaris] p. 90. Also Theorem *10.22 of [WhiteheadRussell] p. 119. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.)
Assertion
Ref Expression
19.26

Proof of Theorem 19.26
StepHypRef Expression
1 simpl 108 . . . 4
21alimi 1432 . . 3
3 simpr 109 . . . 4
43alimi 1432 . . 3
52, 4jca 304 . 2
6 id 19 . . 3
76alanimi 1436 . 2
85, 7impbii 125 1
 Colors of variables: wff set class Syntax hints:   wa 103   wb 104  wal 1330 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  19.26-2  1459  19.26-3an  1460  albiim  1464  2albiim  1465  hband  1466  hban  1523  19.27h  1536  19.27  1537  19.28h  1538  19.28  1539  nford  1543  nfand  1544  equsexd  1703  equveli  1728  sbanv  1857  2eu4  2083  bm1.1  2126  r19.26m  2568  unss  3257  ralunb  3264  ssin  3305  intun  3812  intpr  3813  eqrelrel  4652  relop  4701  eqoprab2b  5841  dfer2  6442  omniwomnimkv  7060
 Copyright terms: Public domain W3C validator