Theorem exim 1853

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 1851	1 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))

Syntax hints:   → wi 4  ∀wal 1557  ∃wex 1798

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

This theorem depends on definitions:  df-bi 209  df-ex 1799

This theorem is referenced by:  eximi  1854  19.38b  1860  19.23v  1961  alequexv  2020  nf5-1  2178  spimt  2416  darii  2690  festino  2699  baroco  2701  darapti  2709  elex22  3477  spcimgfi1OLD  3515  sbccomlem  3822  rspn0  4308  replem  5237  exel  5400  bj-axdd2  36999  bj-2exim  37037  bj-sylget  37040  bj-alexim  37047  bj-aleximiALT  37048  bj-eqs  37112  bj-nnf-exlim  37199  bj-nnflemee  37226  bj-nnflemae  37227  bj-axc10  37232  bj-alequex  37233  bj-spimtv  37243  bj-spcimdv  37344  bj-spcimdvv  37345  bj-axreprepsep  37524  sn-exelALT  42802  2exim  44919  pm11.71  44937  onfrALTlem2  45086  19.41rg  45090  ax6e2nd  45098  elex2VD  45377  elex22VD  45378  onfrALTlem2VD  45428  19.41rgVD  45441  ax6e2eqVD  45446  ax6e2ndVD  45447  ax6e2ndeqVD  45448  ax6e2ndALT  45469  ax6e2ndeqALT  45470