MPE Home 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  |-  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 1754 . 2  |-  ( ph  ->  A. x ph )
3 eximd.2 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
42, 3eximdh 1578 1  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1531   F/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