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

Theorem eximd 1786
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 1778 . 2  |-  ( ph  ->  A. x ph )
3 eximd.2 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
42, 3eximdh 1598 1  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1550   F/wnf 1553
This theorem is referenced by:  exlimd  1824  19.41  1900  19.41OLD  1901  exdistrfOLD  2063  sbiedOLD  2124  mo  2302  mopick2  2347  2euex  2352  copsexg  4434  ssopab2  4472  axextnd  8455  axpowndlem3  8463  axregndlem1  8466  axregnd  8468  finminlem  26258  ssrexf  27598  stoweidlem27  27690  stoweidlem34  27697  stoweidlem35  27698  exdistrfNEW7  29359  sbiedNEW7  29392  pmapglb2xN  30408
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator