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

Theorem eximd 1830
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 1822 . 2  |-  ( ph  ->  A. x ph )
3 eximd.2 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
42, 3eximdh 1650 1  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1596   F/wnf 1599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-12 1803
This theorem depends on definitions:  df-bi 185  df-ex 1597  df-nf 1600
This theorem is referenced by:  exlimd  1861  19.41  1920  sbiedOLD  2126  2ax6elem  2179  mo3OLD  2321  moOLD  2327  mopick2  2370  2euex  2375  reximd2a  2937  copsexgOLD  4738  axpowndlem3  8985  axpowndlem3OLD  8986  axregndlem1  8989  axregnd  8991  axregndOLD  8992  spc2ed  27163  finminlem  30031  ssrexf  31258  islpcn  31472  stoweidlem27  31618  stoweidlem34  31625  stoweidlem35  31626  pmapglb2xN  34861
  Copyright terms: Public domain W3C validator