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

Theorem eximd 1821
Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 29-Jun-1993.) (Revised 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 1813 . 2  |-  ( ph  ->  A. x ph )
3 eximd.2 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
42, 3eximdh 1641 1  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1587   F/wnf 1590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-ex 1588  df-nf 1591
This theorem is referenced by:  exlimd  1852  19.41  1911  sbiedOLD  2113  2ax6elem  2166  mo3OLD  2308  moOLD  2314  mopick2  2357  2euex  2362  copsexgOLD  4688  axpowndlem3  8879  axpowndlem3OLD  8880  axregndlem1  8883  axregnd  8885  axregndOLD  8886  spc2ed  26036  finminlem  28684  ssrexf  29906  stoweidlem27  29993  stoweidlem34  30000  stoweidlem35  30001  pmapglb2xN  33779
  Copyright terms: Public domain W3C validator