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

Theorem exim 1828
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 1826 1 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1531  wex 1773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803
This theorem depends on definitions:  df-bi 206  df-ex 1774
This theorem is referenced by:  eximi  1829  19.38b  1835  19.23v  1937  alequexv  1996  nf5-1  2133  spimt  2379  darii  2653  festino  2662  baroco  2664  darapti  2672  elex2OLD  3485  elex22  3486  vtoclegftOLD  3570  spcimgft  3572  rspn0  4354  exel  5438  bj-axdd2  36245  bj-2exim  36264  bj-sylget  36273  bj-alexim  36279  bj-cbvalimt  36291  bj-cbveximt  36292  bj-eqs  36327  bj-nnf-exlim  36409  bj-nnflemee  36416  bj-nnflemae  36417  bj-axc10  36436  bj-alequex  36437  bj-spimtv  36447  bj-spcimdv  36549  bj-spcimdvv  36550  sn-exelALT  41883  nfa1w  42267  2exim  43990  pm11.71  44008  onfrALTlem2  44159  19.41rg  44163  ax6e2nd  44171  elex2VD  44451  elex22VD  44452  onfrALTlem2VD  44502  19.41rgVD  44515  ax6e2eqVD  44520  ax6e2ndVD  44521  ax6e2ndeqVD  44522  ax6e2ndALT  44543  ax6e2ndeqALT  44544
  Copyright terms: Public domain W3C validator