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

Theorem exim 1750
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 1748 1 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1472  wex 1694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727
This theorem depends on definitions:  df-bi 195  df-ex 1695
This theorem is referenced by:  eximi  1751  19.23v  1888  nf5-1  2009  19.8a  2037  19.8aOLD  2038  19.9ht  2126  spimt  2239  elex2  3187  elex22  3188  vtoclegft  3251  spcimgft  3255  bj-axdd2  31554  bj-2exim  31585  bj-exlimh  31592  bj-sbex  31620  bj-eqs  31655  bj-axc10  31699  bj-alequex  31700  bj-spimtv  31710  bj-spcimdv  31880  wl-nf-nf2  32265  2exim  37402  pm11.71  37421  onfrALTlem2  37584  19.41rg  37589  ax6e2nd  37597  elex2VD  37897  elex22VD  37898  onfrALTlem2VD  37949  19.41rgVD  37962  ax6e2eqVD  37967  ax6e2ndVD  37968  ax6e2ndeqVD  37969  ax6e2ndALT  37990  ax6e2ndeqALT  37991
  Copyright terms: Public domain W3C validator