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

Theorem eximd 1887
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1659. (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 1879 . 2  |-  ( ph  ->  A. x ph )
3 eximd.2 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
42, 3eximdh 1678 1  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1617   F/wnf 1621
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-12 1859
This theorem depends on definitions:  df-bi 185  df-ex 1618  df-nf 1622
This theorem is referenced by:  exlimd  1919  19.41  1976  2ax6elem  2195  mo3OLD  2325  mopick2  2359  2euex  2363  reximd2a  2924  ssrexf  3549  axpowndlem3  8965  axregndlem1  8968  axregnd  8970  axregndOLD  8971  spc2ed  27570  padct  27776  finminlem  30376  islpcn  31884  stoweidlem27  32048  stoweidlem34  32055  stoweidlem35  32056  pmapglb2xN  35893
  Copyright terms: Public domain W3C validator