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

Theorem eximd 1771
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 1763 . 2  |-  ( ph  ->  A. x ph )
3 eximd.2 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
42, 3eximdh 1588 1  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1541   F/wnf 1544
This theorem is referenced by:  exlimd  1807  19.41  1882  19.41OLD  1883  exdistrf  1976  sbied  2041  mo  2231  mopick2  2276  2euex  2281  copsexg  4334  ssopab2  4372  axextnd  8303  axpowndlem3  8311  axregndlem1  8314  axregnd  8316  ishashinf  23363  finminlem  25555  ssrexf  27007  stoweidlem27  27099  stoweidlem34  27106  stoweidlem35  27107  exdistrfNEW7  28928  sbiedNEW7  28961  pmapglb2xN  30030
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746
This theorem depends on definitions:  df-bi 177  df-ex 1542  df-nf 1545
  Copyright terms: Public domain W3C validator