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

Theorem eximd 2215
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1833. (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 2194 . 2 (𝜑 → ∀𝑥𝜑)
3 eximd.2 . 2 (𝜑 → (𝜓𝜒))
42, 3eximdh 1863 1 (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1778  wnf 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-12 2176
This theorem depends on definitions:  df-bi 207  df-ex 1779  df-nf 1783
This theorem is referenced by:  exlimd  2217  19.41  2234  2ax6elem  2474  2euexv  2630  mopick2  2636  2euex  2640  reximd2a  3268  spc2ed  3600  ssrexf  4049  rexdifi  4149  axprlem4OLD  5428  axprlem5OLD  5429  axpowndlem3  10640  axregndlem1  10643  axregnd  10645  padct  32732  dvelimexcased  35092  finminlem  36320  difunieq  37376  wl-euequf  37576  pmapglb2xN  39775  unitscyglem5  42201  infrpge  45367  fsumiunss  45595  islpcn  45659  stoweidlem34  46054  stoweidlem35  46055  sge0rpcpnf  46441
  Copyright terms: Public domain W3C validator