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

Theorem exim 1737
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 1735 1 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1466  wex 1692
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711
This theorem depends on definitions:  df-bi 192  df-ex 1693
This theorem is referenced by:  eximi  1738  19.23v  1850  19.8a  1988  19.8aOLD  1989  19.9ht  2020  19.23tOLD  2045  spimt  2144  elex2  3079  elex22  3080  vtoclegft  3142  spcimgft  3146  bj-axdd2  31359  bj-2exim  31387  bj-exlimh  31393  bj-sbex  31421  bj-eqs  31456  bj-axc10  31495  bj-alequex  31496  bj-spimtv  31506  bj-spcimdv  31677  2exim  37085  pm11.71  37104  onfrALTlem2  37268  19.41rg  37273  ax6e2nd  37281  elex2VD  37582  elex22VD  37583  onfrALTlem2VD  37634  19.41rgVD  37647  ax6e2eqVD  37652  ax6e2ndVD  37653  ax6e2ndeqVD  37654  ax6e2ndALT  37675  ax6e2ndeqALT  37676
  Copyright terms: Public domain W3C validator