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

Theorem 19.26 1680
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 1633 . . 3
3 simpr 461 . . . 4
43alimi 1633 . . 3
52, 4jca 532 . 2
6 id 22 . . 3
76alanimi 1637 . 2
85, 7impbii 188 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369  A.wal 1393
This theorem is referenced by:  19.26-2  1681  19.26-3an  1682  19.35OLD  1688  19.43OLD  1694  albiim  1699  2albiim  1700  19.27v  1766  19.28v  1767  19.27  1923  19.28  1924  ax12eq  2271  ax12el  2272  2eu4OLD  2381  bm1.1OLD  2441  r19.26m  2987  unss  3677  ralunb  3684  ssin  3719  intun  4319  intpr  4320  eqrelrel  5109  relop  5158  eqoprab2b  6355  dfer2  7331  axgroth4  9231  grothprim  9233  caubnd  13191  wl-alanbii  30018  dford4  30971  alimp-no-surprise  33196  bj-gl4lem  34183  bj-gl4  34184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631
This theorem depends on definitions:  df-bi 185  df-an 371
  Copyright terms: Public domain W3C validator