MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  19.26 Unicode version

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

Proof of Theorem 19.26
StepHypRef Expression
1 simpl 457 . . . 4
21alimi 1605 . . 3
3 simpr 461 . . . 4
43alimi 1605 . . 3
52, 4jca 532 . 2
6 id 22 . . 3
76alanimi 1608 . 2
85, 7impbii 188 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369  A.wal 1368
This theorem is referenced by:  19.26-2  1649  19.26-3an  1650  19.35OLD  1656  19.43OLD  1662  albiim  1666  2albiim  1667  19.27  1857  19.28  1858  ax12eq  2248  ax12el  2249  2eu4OLD  2375  bm1.1OLD  2434  r19.26m  2932  unss  3612  ralunb  3619  ssin  3654  intun  4242  intpr  4243  eqrelrel  5023  relop  5072  eqoprab2b  6227  dfer2  7186  axgroth4  9084  grothprim  9086  caubnd  12932  wl-alanbii  28516  dford4  29500  alimp-no-surprise  31414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603
This theorem depends on definitions:  df-bi 185  df-an 371
  Copyright terms: Public domain W3C validator