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

Theorem eximd 1711
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 1703 . 2  |-  ( ph  ->  A. x ph )
3 eximd.2 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
42, 3eximdh 1586 1  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6   E.wex 1537   F/wnf 1539
This theorem is referenced by:  19.41  1799  exdistrf  1864  sbied  1909  eximdv  2019  mo  2138  mopick2  2183  2euex  2188  copsexg  4189  ssopab2  4227  axextnd  8146  axpowndlem3  8154  axregndlem1  8157  axregnd  8159  finminlem  25563  ssrexf  27017  stoweidlem27  27076  stoweidlem34  27083  stoweidlem35  27084  pmapglb2xN  29091
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-ex 1538  df-nf 1540
  Copyright terms: Public domain W3C validator