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

Theorem exim 1833
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 1831 1 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1537  wex 1778
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808
This theorem depends on definitions:  df-bi 207  df-ex 1779
This theorem is referenced by:  eximi  1834  19.38b  1840  19.23v  1941  alequexv  1999  nf5-1  2144  spimt  2390  darii  2664  festino  2673  baroco  2675  darapti  2683  elex2OLD  3504  elex22  3505  spcimgfi1OLD  3547  vtoclegftOLD  3588  sbccomlem  3868  rspn0  4355  exel  5437  bj-axdd2  36594  bj-2exim  36613  bj-sylget  36623  bj-alexim  36629  bj-cbvalimt  36641  bj-cbveximt  36642  bj-eqs  36677  bj-nnf-exlim  36758  bj-nnflemee  36765  bj-nnflemae  36766  bj-axc10  36785  bj-alequex  36786  bj-spimtv  36796  bj-spcimdv  36897  bj-spcimdvv  36898  sn-exelALT  42258  2exim  44403  pm11.71  44421  onfrALTlem2  44571  19.41rg  44575  ax6e2nd  44583  elex2VD  44863  elex22VD  44864  onfrALTlem2VD  44914  19.41rgVD  44927  ax6e2eqVD  44932  ax6e2ndVD  44933  ax6e2ndeqVD  44934  ax6e2ndALT  44955  ax6e2ndeqALT  44956
  Copyright terms: Public domain W3C validator