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

Theorem exim 1835
 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 1833 1 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1536  ∃wex 1781 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811 This theorem depends on definitions:  df-bi 210  df-ex 1782 This theorem is referenced by:  eximi  1836  19.38b  1842  19.23v  1944  alequexv  2008  spsbeOLD  2090  nf5-1  2150  spimt  2406  darii  2753  festino  2762  baroco  2764  darapti  2772  elex2  3502  elex22  3503  vtoclegft  3568  spcimgft  3572  bj-axdd2  33953  bj-2exim  33972  bj-sylget  33981  bj-alexim  33987  bj-cbvalimt  33999  bj-cbveximt  34000  bj-eqs  34035  bj-nnf-exlim  34114  bj-nnflemee  34121  bj-nnflemae  34122  bj-axc10  34134  bj-alequex  34135  bj-spimtv  34145  bj-spcimdv  34249  bj-spcimdvv  34250  sn-el  39284  2exim  40943  pm11.71  40961  onfrALTlem2  41112  19.41rg  41116  ax6e2nd  41124  elex2VD  41404  elex22VD  41405  onfrALTlem2VD  41455  19.41rgVD  41468  ax6e2eqVD  41473  ax6e2ndVD  41474  ax6e2ndeqVD  41475  ax6e2ndALT  41496  ax6e2ndeqALT  41497
 Copyright terms: Public domain W3C validator