Theorem exim 1841

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 22	. 2 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜓))
2	1	aleximi 1839	1 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))

Syntax hints:   → wi 4  ∀wal 1545  ∃wex 1786

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

This theorem depends on definitions:  df-bi 208  df-ex 1787

This theorem is referenced by:  eximi  1842  19.38b  1848  19.23v  1949  alequexv  2008  nf5-1  2156  spimt  2394  darii  2669  festino  2678  baroco  2680  darapti  2688  elex22  3457  spcimgfi1OLD  3496  sbccomlem  3808  rspn0  4291  replem  5217  exel  5380  bj-axdd2  36910  bj-2exim  36948  bj-sylget  36951  bj-alexim  36958  bj-aleximiALT  36959  bj-eqs  37023  bj-nnf-exlim  37110  bj-nnflemee  37137  bj-nnflemae  37138  bj-axc10  37143  bj-alequex  37144  bj-spimtv  37154  bj-spcimdv  37255  bj-spcimdvv  37256  bj-axreprepsep  37435  sn-exelALT  42713  2exim  44830  pm11.71  44848  onfrALTlem2  44997  19.41rg  45001  ax6e2nd  45009  elex2VD  45288  elex22VD  45289  onfrALTlem2VD  45339  19.41rgVD  45352  ax6e2eqVD  45357  ax6e2ndVD  45358  ax6e2ndeqVD  45359  ax6e2ndALT  45380  ax6e2ndeqALT  45381