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

Theorem exim 1837
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 1835 1 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1540  wex 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812
This theorem depends on definitions:  df-bi 206  df-ex 1783
This theorem is referenced by:  eximi  1838  19.38b  1844  19.23v  1946  alequexv  2005  nf5-1  2142  spimt  2386  darii  2661  festino  2670  baroco  2672  darapti  2680  elex2OLD  3496  elex22  3497  vtoclegftOLD  3575  spcimgft  3578  rspn0  4353  exel  5434  bj-axdd2  35470  bj-2exim  35489  bj-sylget  35498  bj-alexim  35504  bj-cbvalimt  35516  bj-cbveximt  35517  bj-eqs  35552  bj-nnf-exlim  35634  bj-nnflemee  35641  bj-nnflemae  35642  bj-axc10  35661  bj-alequex  35662  bj-spimtv  35672  bj-spcimdv  35775  bj-spcimdvv  35776  sn-exelALT  41035  2exim  43138  pm11.71  43156  onfrALTlem2  43307  19.41rg  43311  ax6e2nd  43319  elex2VD  43599  elex22VD  43600  onfrALTlem2VD  43650  19.41rgVD  43663  ax6e2eqVD  43668  ax6e2ndVD  43669  ax6e2ndeqVD  43670  ax6e2ndALT  43691  ax6e2ndeqALT  43692
  Copyright terms: Public domain W3C validator