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

Theorem eximd 2210
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1837. (Contributed by NM, 29-Jun-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
eximd.1 𝑥𝜑
eximd.2 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
eximd (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))

Proof of Theorem eximd
StepHypRef Expression
1 eximd.1 . . 3 𝑥𝜑
21nf5ri 2189 . 2 (𝜑 → ∀𝑥𝜑)
3 eximd.2 . 2 (𝜑 → (𝜓𝜒))
42, 3eximdh 1868 1 (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1782  wnf 1786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172
This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787
This theorem is referenced by:  exlimd  2212  19.41  2229  2ax6elem  2469  2euexv  2632  mopick2  2638  2euex  2642  reximd2a  3255  spc2ed  3563  ssrexf  4013  rexdifi  4110  axprlem4  5386  axprlem5  5387  axpowndlem3  10542  axregndlem1  10545  axregnd  10547  padct  31678  finminlem  34819  difunieq  35874  wl-euequf  36058  pmapglb2xN  38264  infrpge  43659  fsumiunss  43890  islpcn  43954  stoweidlem34  44349  stoweidlem35  44350  sge0rpcpnf  44736
  Copyright terms: Public domain W3C validator