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

Theorem 19.41 1971
Description: Theorem 19.41 of [Margaris] p. 90. See 19.41v 1771 for a version requiring fewer axioms. (Contributed by NM, 14-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 12-Jan-2018.)
Hypothesis
Ref Expression
19.41.1
Assertion
Ref Expression
19.41

Proof of Theorem 19.41
StepHypRef Expression
1 19.40 1679 . . 3
2 19.41.1 . . . . 5
3219.9 1893 . . . 4
43anbi2i 694 . . 3
51, 4sylib 196 . 2
6 pm3.21 448 . . . 4
72, 6eximd 1882 . . 3
87impcom 430 . 2
95, 8impbii 188 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369  E.wex 1612  F/wnf 1616
This theorem is referenced by:  19.42  1972  exan  1973  eean  1987  eeeanv  1989  2sb5rf  2195  r19.41  3010  eliunxp  5145  dfopab2  6854  dfoprab3s  6855  xpcomco  7627  mpt2mptxf  27518  eliunxp2  32923  2sb5nd  33333  2sb5ndVD  33710  2sb5ndALT  33732  bnj605  33965  bnj607  33974
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617
  Copyright terms: Public domain W3C validator