Theorem exim 1864

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

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜓))
2	1	aleximi 1862	1 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))

Syntax hints:   → wi 4  ∀wal 1568  ∃wex 1809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839

This theorem depends on definitions:  df-bi 210  df-ex 1810

This theorem is referenced by:  eximi  1865  19.38b  1871  19.23v  1972  alequexv  2031  nf5-1  2180  spimt  2418  darii  2692  festino  2701  baroco  2703  darapti  2711  elex22  3479  spcimgfi1OLD  3517  sbccomlem  3823  rspn0  4312  replem  5250  exel  5417  bj-axdd2  37163  bj-2exim  37201  bj-sylget  37204  bj-alexim  37211  bj-aleximiALT  37212  bj-eqs  37276  bj-nnf-exlim  37363  bj-nnflemee  37390  bj-nnflemae  37391  bj-axc10  37396  bj-alequex  37397  bj-spimtv  37407  bj-spcimdv  37508  bj-spcimdvv  37509  bj-axreprepsep  37690  sn-exelALT  42968  2exim  45069  pm11.71  45087  onfrALTlem2  45235  19.41rg  45239  ax6e2nd  45247  elex2VD  45526  elex22VD  45527  onfrALTlem2VD  45577  19.41rgVD  45590  ax6e2eqVD  45595  ax6e2ndVD  45596  ax6e2ndeqVD  45597  ax6e2ndALT  45618  ax6e2ndeqALT  45619  alsex  50553