MPE Home 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  |-  F/ x ph
eximd.2  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
eximd  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)

Proof of Theorem eximd
StepHypRef Expression
1 eximd.1 . . 3  |-  F/ x ph
21nfri 1779 . 2  |-  ( ph  ->  A. x ph )
3 eximd.2 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
42, 3eximdh 1599 1  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1551   F/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