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

Theorem eximd 2206
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1825. (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 2185 . 2 (𝜑 → ∀𝑥𝜑)
3 eximd.2 . 2 (𝜑 → (𝜓𝜒))
42, 3eximdh 1856 1 (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1771  wnf 1775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-12 2167
This theorem depends on definitions:  df-bi 208  df-ex 1772  df-nf 1776
This theorem is referenced by:  exlimd  2208  19.41  2227  2ax6elem  2485  sbimdOLD  2511  2euexv  2709  mopick2  2715  2euex  2719  reximd2a  3309  spc2ed  3599  ssrexf  4028  rexdifi  4119  axprlem4  5317  axprlem5  5318  axpowndlem3  10009  axregndlem1  10012  axregnd  10014  padct  30381  finminlem  33563  difunieq  34537  wl-euequf  34691  pmapglb2xN  36788  disjinfi  41330  infrpge  41495  fsumiunss  41732  islpcn  41796  stoweidlem34  42196  stoweidlem35  42197  sge0rpcpnf  42580
  Copyright terms: Public domain W3C validator