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

Theorem eximd 1762
 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 1754 . 2
3 eximd.2 . 2
42, 3eximdh 1578 1
 Colors of variables: wff set class Syntax hints:   wi 4  wex 1531  wnf 1534 This theorem is referenced by:  19.41  1827  exdistrf  1924  sbied  1989  mo  2178  mopick2  2223  2euex  2228  copsexg  4268  ssopab2  4306  axextnd  8229  axpowndlem3  8237  axregndlem1  8240  axregnd  8242  ishashinf  23404  finminlem  26334  ssrexf  27787  stoweidlem27  27879  stoweidlem34  27886  stoweidlem35  27887  exdistrfNEW7  29482  sbiedNEW7  29515  pmapglb2xN  30583 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727 This theorem depends on definitions:  df-bi 177  df-ex 1532  df-nf 1535
 Copyright terms: Public domain W3C validator