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

Theorem exim 1836
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 1834 1 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1539  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 206  df-ex 1782
This theorem is referenced by:  eximi  1837  19.38b  1843  19.23v  1945  alequexv  2004  nf5-1  2141  spimt  2385  darii  2660  festino  2669  baroco  2671  darapti  2679  elex2OLD  3495  elex22  3496  vtoclegftOLD  3574  spcimgft  3577  rspn0  4351  exel  5432  bj-axdd2  35458  bj-2exim  35477  bj-sylget  35486  bj-alexim  35492  bj-cbvalimt  35504  bj-cbveximt  35505  bj-eqs  35540  bj-nnf-exlim  35622  bj-nnflemee  35629  bj-nnflemae  35630  bj-axc10  35649  bj-alequex  35650  bj-spimtv  35660  bj-spcimdv  35763  bj-spcimdvv  35764  sn-exelALT  41031  2exim  43123  pm11.71  43141  onfrALTlem2  43292  19.41rg  43296  ax6e2nd  43304  elex2VD  43584  elex22VD  43585  onfrALTlem2VD  43635  19.41rgVD  43648  ax6e2eqVD  43653  ax6e2ndVD  43654  ax6e2ndeqVD  43655  ax6e2ndALT  43676  ax6e2ndeqALT  43677
  Copyright terms: Public domain W3C validator