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

Theorem exim 1831
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 1829 1 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1535  wex 1776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806
This theorem depends on definitions:  df-bi 207  df-ex 1777
This theorem is referenced by:  eximi  1832  19.38b  1838  19.23v  1940  alequexv  1998  nf5-1  2143  spimt  2389  darii  2663  festino  2672  baroco  2674  darapti  2682  elex2OLD  3503  elex22  3504  spcimgfi1OLD  3548  vtoclegftOLD  3589  sbccomlem  3878  rspn0  4362  exel  5444  bj-axdd2  36575  bj-2exim  36594  bj-sylget  36604  bj-alexim  36610  bj-cbvalimt  36622  bj-cbveximt  36623  bj-eqs  36658  bj-nnf-exlim  36739  bj-nnflemee  36746  bj-nnflemae  36747  bj-axc10  36766  bj-alequex  36767  bj-spimtv  36777  bj-spcimdv  36878  bj-spcimdvv  36879  sn-exelALT  42236  2exim  44375  pm11.71  44393  onfrALTlem2  44544  19.41rg  44548  ax6e2nd  44556  elex2VD  44836  elex22VD  44837  onfrALTlem2VD  44887  19.41rgVD  44900  ax6e2eqVD  44905  ax6e2ndVD  44906  ax6e2ndeqVD  44907  ax6e2ndALT  44928  ax6e2ndeqALT  44929
  Copyright terms: Public domain W3C validator