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

Theorem exim 1751
 Description: Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.)
Assertion
Ref Expression
exim (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))

Proof of Theorem exim
StepHypRef Expression
1 id 22 . 2 ((𝜑𝜓) → (𝜑𝜓))
21aleximi 1749 1 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1473  ∃wex 1695 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728 This theorem depends on definitions:  df-bi 196  df-ex 1696 This theorem is referenced by:  eximi  1752  19.23v  1889  nf5-1  2010  19.8a  2039  19.8aOLD  2040  19.9ht  2128  spimt  2241  elex2  3189  elex22  3190  vtoclegft  3253  spcimgft  3257  bj-axdd2  31749  bj-2exim  31780  bj-exlimh  31787  bj-sbex  31815  bj-eqs  31850  bj-axc10  31894  bj-alequex  31895  bj-spimtv  31905  bj-spcimdv  32078  wl-nf-nf2  32463  2exim  37600  pm11.71  37619  onfrALTlem2  37782  19.41rg  37787  ax6e2nd  37795  elex2VD  38095  elex22VD  38096  onfrALTlem2VD  38147  19.41rgVD  38160  ax6e2eqVD  38165  ax6e2ndVD  38166  ax6e2ndeqVD  38167  ax6e2ndALT  38188  ax6e2ndeqALT  38189
 Copyright terms: Public domain W3C validator