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  2183  spimt  2421  darii  2695  festino  2704  baroco  2706  darapti  2714  elex22  3482  sbccomlem  3825  rspn0  4314  replem  5254  exel  5420  bj-axdd2  37226  bj-2exim  37264  bj-sylget  37267  bj-alexim  37274  bj-aleximiALT  37275  bj-eqs  37339  bj-nnf-exlim  37426  bj-nnflemee  37453  bj-nnflemae  37454  bj-axc10  37459  bj-alequex  37460  bj-spimtv  37470  bj-spcimdv  37571  bj-spcimdvv  37572  bj-axreprepsep  37753  sn-exelALT  43031  2exim  45130  pm11.71  45148  onfrALTlem2  45296  19.41rg  45300  ax6e2nd  45308  elex2VD  45587  elex22VD  45588  onfrALTlem2VD  45638  19.41rgVD  45651  ax6e2eqVD  45656  ax6e2ndVD  45657  ax6e2ndeqVD  45658  ax6e2ndALT  45679  ax6e2ndeqALT  45680  alsex  50617