Theorem exim 1866

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1567  ∃wex 1811

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

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

This theorem is used by:  eximi  1867  19.38b  1873  19.23v  1974  alequexv  2033  nf5-1  2181  spimt  2415  darii  2689  festino  2698  baroco  2700  darapti  2708  elex22  3474  sbccomlem  3816  rspn0  4303  replem  5240  exel  5401  bj-axdd2  37554  bj-2exim  37592  bj-sylget  37595  bj-alexim  37602  bj-aleximiALT  37603  bj-eqs  37667  bj-nnf-exlim  37754  bj-nnflemee  37781  bj-nnflemae  37782  bj-axc10  37787  bj-alequex  37788  bj-spimtv  37798  bj-spcimdv  37899  bj-spcimdvv  37900  bj-axreprepsep  38083  sn-exelALT  43366  2exim  45456  pm11.71  45474  onfrALTlem2  45622  19.41rg  45626  ax6e2nd  45634  elex2VD  45913  elex22VD  45914  onfrALTlem2VD  45964  19.41rgVD  45977  ax6e2eqVD  45982  ax6e2ndVD  45983  ax6e2ndeqVD  45984  ax6e2ndALT  46005  ax6e2ndeqALT  46006  alsex  51062