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

Theorem eximd 1866
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1639. (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 1858 . 2  |-  ( ph  ->  A. x ph )
3 eximd.2 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
42, 3eximdh 1658 1  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1597   F/wnf 1601
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-12 1838
This theorem depends on definitions:  df-bi 185  df-ex 1598  df-nf 1602
This theorem is referenced by:  exlimd  1898  19.41  1955  2ax6elem  2177  mo3OLD  2308  mopick2  2346  2euex  2350  reximd2a  2911  copsexgOLD  4719  axpowndlem3  8973  axpowndlem3OLD  8974  axregndlem1  8977  axregnd  8979  axregndOLD  8980  spc2ed  27237  finminlem  30104  ssrexf  31335  islpcn  31549  stoweidlem27  31694  stoweidlem34  31701  stoweidlem35  31702  pmapglb2xN  35198
  Copyright terms: Public domain W3C validator