Theorem exim 1867

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  eximi  1868  19.38b  1874  19.23v  1975  alequexv  2034  nf5-1  2182  spimt  2417  darii  2691  festino  2700  baroco  2702  darapti  2710  elex22  3477  sbccomlem  3820  rspn0  4307  replem  5247  exel  5413  bj-axdd2  37301  bj-2exim  37339  bj-sylget  37342  bj-alexim  37349  bj-aleximiALT  37350  bj-eqs  37414  bj-nnf-exlim  37501  bj-nnflemee  37528  bj-nnflemae  37529  bj-axc10  37534  bj-alequex  37535  bj-spimtv  37545  bj-spcimdv  37646  bj-spcimdvv  37647  bj-axreprepsep  37828  sn-exelALT  43097  2exim  45211  pm11.71  45229  onfrALTlem2  45377  19.41rg  45381  ax6e2nd  45389  elex2VD  45668  elex22VD  45669  onfrALTlem2VD  45719  19.41rgVD  45732  ax6e2eqVD  45737  ax6e2ndVD  45738  ax6e2ndeqVD  45739  ax6e2ndALT  45760  ax6e2ndeqALT  45761  alsex  50735