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

Theorem exim 1898
 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 1896 1 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1618  ∃wex 1841 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874 This theorem depends on definitions:  df-bi 197  df-ex 1842 This theorem is referenced by:  eximi  1899  19.38b  1905  19.23v  2008  19.23vOLD  2056  nf5-1  2160  19.8a  2187  19.9ht  2278  spimt  2386  elex2  3344  elex22  3345  vtoclegft  3408  spcimgft  3412  bj-axdd2  32853  bj-2exim  32872  bj-exlimh  32879  bj-alexim  32882  bj-sbex  32903  bj-alequexv  32932  bj-eqs  32940  bj-axc10  32984  bj-alequex  32985  bj-spimtv  32995  bj-spcimdv  33161  bj-spcimdvv  33162  2exim  39049  pm11.71  39068  onfrALTlem2  39232  19.41rg  39237  ax6e2nd  39245  elex2VD  39541  elex22VD  39542  onfrALTlem2VD  39593  19.41rgVD  39606  ax6e2eqVD  39611  ax6e2ndVD  39612  ax6e2ndeqVD  39613  ax6e2ndALT  39634  ax6e2ndeqALT  39635
 Copyright terms: Public domain W3C validator