Theorem exim 1487

Description: Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.)

Assertion

Ref	Expression
exim	⊢ (∀x(φ → ψ) → (∃xφ → ∃xψ))

Proof of Theorem exim

Step	Hyp	Ref	Expression
1		hba1 1430	. 2 ⊢ (∀x(φ → ψ) → ∀x∀x(φ → ψ))
2		hbe1 1381	. 2 ⊢ (∃xψ → ∀x∃xψ)
3		19.8a 1479	. . . 4 ⊢ (ψ → ∃xψ)
4	3	imim2i 12	. . 3 ⊢ ((φ → ψ) → (φ → ∃xψ))
5	4	sps 1427	. 2 ⊢ (∀x(φ → ψ) → (φ → ∃xψ))
6	1, 2, 5	exlimdh 1484	1 ⊢ (∀x(φ → ψ) → (∃xφ → ∃xψ))

Syntax hints:   → wi 4  ∀wal 1240  ∃wex 1378

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-ial 1424

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  eximi  1488  exbi  1492  eximdh  1499  19.29  1508  19.25  1514  alexim  1533  19.23t  1564  spimt  1621  equvini  1638  nfexd  1641  ax10oe  1675  sbcof2  1688  spsbim  1721  mor  1939  rexim  2407  elex22  2563  elex2  2564  vtoclegft  2619  spcimgft  2623  spcimegft  2625  spc2gv  2637  spc3gv  2639  ssoprab2  5503  bj-inf2vnlem1  9354