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  1977  alequexv  2036  nf5-1  2185  spimt  2418  darii  2692  festino  2701  baroco  2703  darapti  2711  elex22  3478  sbccomlem  3821  rspn0  4307  replem  5244  exel  5406  bj-axdd2  37640  bj-2exim  37678  bj-sylget  37681  bj-alexim  37688  bj-aleximiALT  37689  bj-eqs  37753  bj-nnf-exlim  37840  bj-nnflemee  37867  bj-nnflemae  37868  bj-axc10  37873  bj-alequex  37874  bj-spimtv  37884  bj-spcimdv  37985  bj-spcimdvv  37986  bj-axreprepsep  38182  sn-exelALT  43466  2exim  45555  pm11.71  45573  onfrALTlem2  45720  19.41rg  45724  ax6e2nd  45732  elex2VD  46011  elex22VD  46012  onfrALTlem2VD  46062  19.41rgVD  46075  ax6e2eqVD  46080  ax6e2ndVD  46081  ax6e2ndeqVD  46082  ax6e2ndALT  46103  ax6e2ndeqALT  46104  alsex  51174