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

Theorem exim 1909
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 1907 1 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1629  wex 1852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885
This theorem depends on definitions:  df-bi 197  df-ex 1853
This theorem is referenced by:  eximi  1910  19.38b  1917  19.38bOLD  1918  19.23v  2023  19.23vOLD  2071  nf5-1  2178  19.8a  2206  19.9ht  2308  spimt  2415  elex2  3368  elex22  3369  vtoclegft  3432  spcimgft  3436  bj-axdd2  32914  bj-2exim  32933  bj-exlimh  32940  bj-alexim  32943  bj-sbex  32965  bj-alequexv  32993  bj-eqs  33001  bj-axc10  33045  bj-alequex  33046  bj-spimtv  33056  bj-spcimdv  33214  bj-spcimdvv  33215  2exim  39105  pm11.71  39124  onfrALTlem2  39287  19.41rg  39292  ax6e2nd  39300  elex2VD  39596  elex22VD  39597  onfrALTlem2VD  39648  19.41rgVD  39661  ax6e2eqVD  39666  ax6e2ndVD  39667  ax6e2ndeqVD  39668  ax6e2ndALT  39689  ax6e2ndeqALT  39690
  Copyright terms: Public domain W3C validator