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

Theorem eximd 2208
 Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1827. (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 2187 . 2 (𝜑 → ∀𝑥𝜑)
3 eximd.2 . 2 (𝜑 → (𝜓𝜒))
42, 3eximdh 1858 1 (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∃wex 1773  Ⅎwnf 1777 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-12 2169 This theorem depends on definitions:  df-bi 209  df-ex 1774  df-nf 1778 This theorem is referenced by:  exlimd  2210  19.41  2229  2ax6elem  2486  sbimdOLD  2512  2euexv  2710  mopick2  2716  2euex  2720  reximd2a  3310  spc2ed  3600  ssrexf  4029  rexdifi  4120  axprlem4  5317  axprlem5  5318  axpowndlem3  10013  axregndlem1  10016  axregnd  10018  padct  30447  finminlem  33654  difunieq  34642  wl-euequf  34797  pmapglb2xN  36895  disjinfi  41438  infrpge  41603  fsumiunss  41840  islpcn  41904  stoweidlem34  42304  stoweidlem35  42305  sge0rpcpnf  42688
 Copyright terms: Public domain W3C validator