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

Theorem exim 1825
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 1823 1 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1526  wex 1771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801
This theorem depends on definitions:  df-bi 208  df-ex 1772
This theorem is referenced by:  eximi  1826  19.38b  1832  19.23v  1934  alequexv  1998  spsbeOLD  2080  nf5-1  2140  spimt  2395  darii  2745  festino  2754  baroco  2756  darapti  2764  elex2  3514  elex22  3515  vtoclegft  3579  spcimgft  3583  bj-axdd2  33823  bj-2exim  33842  bj-sylget  33851  bj-alexim  33857  bj-cbvalimt  33869  bj-cbveximt  33870  bj-eqs  33905  bj-nnf-exlim  33982  bj-nnflemee  33989  bj-nnflemae  33990  bj-axc10  34002  bj-alequex  34003  bj-spimtv  34013  bj-spcimdv  34108  bj-spcimdvv  34109  sn-el  38988  2exim  40588  pm11.71  40606  onfrALTlem2  40757  19.41rg  40761  ax6e2nd  40769  elex2VD  41049  elex22VD  41050  onfrALTlem2VD  41100  19.41rgVD  41113  ax6e2eqVD  41118  ax6e2ndVD  41119  ax6e2ndeqVD  41120  ax6e2ndALT  41141  ax6e2ndeqALT  41142
  Copyright terms: Public domain W3C validator