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

Theorem eximd 2214
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1831. (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 2193 . 2 (𝜑 → ∀𝑥𝜑)
3 eximd.2 . 2 (𝜑 → (𝜓𝜒))
42, 3eximdh 1862 1 (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1776  wnf 1780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-12 2175
This theorem depends on definitions:  df-bi 207  df-ex 1777  df-nf 1781
This theorem is referenced by:  exlimd  2216  19.41  2233  2ax6elem  2473  2euexv  2629  mopick2  2635  2euex  2639  reximd2a  3267  spc2ed  3601  ssrexf  4062  rexdifi  4160  axprlem4OLD  5435  axprlem5OLD  5436  axpowndlem3  10637  axregndlem1  10640  axregnd  10642  padct  32737  dvelimexcased  35070  finminlem  36301  difunieq  37357  wl-euequf  37555  pmapglb2xN  39755  unitscyglem5  42181  infrpge  45301  fsumiunss  45531  islpcn  45595  stoweidlem34  45990  stoweidlem35  45991  sge0rpcpnf  46377
  Copyright terms: Public domain W3C validator