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

Theorem exim 1739
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 1737 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 1700  ax-4 1713
This theorem depends on definitions:  df-bi 195  df-ex 1695
This theorem is referenced by:  eximi  1740  19.23v  1852  19.8a  1988  19.8aOLD  1989  19.9ht  2019  spimt  2144  elex2  3093  elex22  3094  vtoclegft  3157  spcimgft  3161  bj-axdd2  31584  bj-2exim  31615  bj-exlimh  31622  bj-sbex  31650  bj-eqs  31685  bj-axc10  31729  bj-alequex  31730  bj-spimtv  31740  bj-spcimdv  31910  wl-nf-nf2  32310  wl-dfnf-1  32318  2exim  37482  pm11.71  37501  onfrALTlem2  37664  19.41rg  37669  ax6e2nd  37677  elex2VD  37977  elex22VD  37978  onfrALTlem2VD  38029  19.41rgVD  38042  ax6e2eqVD  38047  ax6e2ndVD  38048  ax6e2ndeqVD  38049  ax6e2ndALT  38070  ax6e2ndeqALT  38071
  Copyright terms: Public domain W3C validator