MPE Home 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  3202  elex22  3203  vtoclegft  3266  spcimgft  3270  bj-axdd2  32215  bj-2exim  32234  bj-exlimh  32241  bj-alexim  32244  bj-sbex  32265  bj-alequexv  32294  bj-eqs  32302  bj-axc10  32346  bj-alequex  32347  bj-spimtv  32357  bj-spcimdv  32528  bj-spcimdvv  32529  2exim  38057  pm11.71  38076  onfrALTlem2  38240  19.41rg  38245  ax6e2nd  38253  elex2VD  38553  elex22VD  38554  onfrALTlem2VD  38605  19.41rgVD  38618  ax6e2eqVD  38623  ax6e2ndVD  38624  ax6e2ndeqVD  38625  ax6e2ndALT  38646  ax6e2ndeqALT  38647
  Copyright terms: Public domain W3C validator