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

Theorem eximd 1787
 Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
eximd.1
eximd.2
Assertion
Ref Expression
eximd

Proof of Theorem eximd
StepHypRef Expression
1 eximd.1 . . 3
21nfri 1779 . 2
3 eximd.2 . 2
42, 3eximdh 1599 1
 Colors of variables: wff set class Syntax hints:   wi 4  wex 1551  wnf 1554 This theorem is referenced by:  exlimd  1825  19.41  1901  19.41OLD  1902  exdistrfOLD  2068  sbied  2151  mo  2305  mopick2  2350  2euex  2355  copsexg  4445  ssopab2  4483  axextnd  8471  axpowndlem3  8479  axregndlem1  8482  axregnd  8484  finminlem  26335  ssrexf  27674  stoweidlem27  27766  stoweidlem34  27773  stoweidlem35  27774  exdistrfNEW7  29579  sbiedNEW7  29614  pmapglb2xN  30643 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762 This theorem depends on definitions:  df-bi 179  df-ex 1552  df-nf 1555
 Copyright terms: Public domain W3C validator