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  4210  ssopab2  4248  axextnd  8167  axpowndlem3  8175  axregndlem1  8178  axregnd  8180  finminlem  25584  ssrexf  27038  stoweidlem27  27097  stoweidlem34  27104  stoweidlem35  27105  pmapglb2xN  29112
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