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  2416  darii  2690  festino  2699  baroco  2701  darapti  2709  elex22  3475  sbccomlem  3817  rspn0  4304  replem  5241  exel  5402  bj-axdd2  37432  bj-2exim  37470  bj-sylget  37473  bj-alexim  37480  bj-aleximiALT  37481  bj-eqs  37545  bj-nnf-exlim  37632  bj-nnflemee  37659  bj-nnflemae  37660  bj-axc10  37665  bj-alequex  37666  bj-spimtv  37676  bj-spcimdv  37777  bj-spcimdvv  37778  bj-axreprepsep  37959  sn-exelALT  43241  2exim  45322  pm11.71  45340  onfrALTlem2  45488  19.41rg  45492  ax6e2nd  45500  elex2VD  45779  elex22VD  45780  onfrALTlem2VD  45830  19.41rgVD  45843  ax6e2eqVD  45848  ax6e2ndVD  45849  ax6e2ndeqVD  45850  ax6e2ndALT  45871  ax6e2ndeqALT  45872  alsex  50838