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

Theorem exim 1934
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 1932 1 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1656  wex 1880
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910
This theorem depends on definitions:  df-bi 199  df-ex 1881
This theorem is referenced by:  eximi  1935  19.38b  1942  19.38bOLD  1943  19.23v  2043  19.23vOLD  2092  exsbim  2108  nf5-1  2198  19.8a  2225  19.9ht  2353  spimt  2407  spimtOLD  2408  darii  2749  festino  2760  baroco  2762  darapti  2774  elex2  3434  elex22  3435  vtoclegft  3498  spcimgft  3502  bj-axdd2  33106  bj-2exim  33125  bj-exlimh  33132  bj-exlalrim  33134  bj-alexim  33135  bj-cbvalimt  33149  bj-sbex  33164  bj-alequexv  33191  bj-eqs  33199  bj-axc10  33242  bj-alequex  33243  bj-spimtv  33253  bj-spcimdv  33405  bj-spcimdvv  33406  2exim  39419  pm11.71  39438  onfrALTlem2  39591  19.41rg  39595  ax6e2nd  39603  elex2VD  39893  elex22VD  39894  onfrALTlem2VD  39944  19.41rgVD  39957  ax6e2eqVD  39962  ax6e2ndVD  39963  ax6e2ndeqVD  39964  ax6e2ndALT  39985  ax6e2ndeqALT  39986
  Copyright terms: Public domain W3C validator