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

Theorem exim 1758
 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 1756 1 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1478  ∃wex 1701 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734 This theorem depends on definitions:  df-bi 197  df-ex 1702 This theorem is referenced by:  eximi  1759  19.38b  1765  19.23v  1899  nf5-1  2020  19.8a  2049  19.8aOLD  2050  19.9ht  2139  spimt  2252  elex2  3206  elex22  3207  vtoclegft  3270  spcimgft  3274  bj-axdd2  32271  bj-2exim  32290  bj-exlimh  32297  bj-alexim  32300  bj-sbex  32321  bj-alequexv  32350  bj-eqs  32358  bj-axc10  32402  bj-alequex  32403  bj-spimtv  32413  bj-spcimdv  32584  bj-spcimdvv  32585  2exim  38099  pm11.71  38118  onfrALTlem2  38282  19.41rg  38287  ax6e2nd  38295  elex2VD  38595  elex22VD  38596  onfrALTlem2VD  38647  19.41rgVD  38660  ax6e2eqVD  38665  ax6e2ndVD  38666  ax6e2ndeqVD  38667  ax6e2ndALT  38688  ax6e2ndeqALT  38689
 Copyright terms: Public domain W3C validator