Theorem exim 1472

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 1415	. 2 ⊢ (∀x(φ → ψ) → ∀x∀x(φ → ψ))
2		hbe1 1365	. 2 ⊢ (∃xψ → ∀x∃xψ)
3		19.8a 1464	. . . 4 ⊢ (ψ → ∃xψ)
4	3	imim2i 12	. . 3 ⊢ ((φ → ψ) → (φ → ∃xψ))
5	4	sps 1412	. 2 ⊢ (∀x(φ → ψ) → (φ → ∃xψ))
6	1, 2, 5	exlimdh 1469	1 ⊢ (∀x(φ → ψ) → (∃xφ → ∃xψ))

Syntax hints:   → wi 4  ∀wal 1226  ∃wex 1362

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 1316  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-4 1381  ax-ial 1409

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  eximi  1473  exbi  1477  eximdh  1484  19.29  1493  19.25  1499  alexim  1518  19.23t  1549  spimt  1606  equvini  1623  nfexd  1626  ax10oe  1660  sbcof2  1673  spsbim  1706  mor  1924  rexim  2391  elex22  2546  elex2  2547  vtoclegft  2602  spcimgft  2606  spcimegft  2608  spc2gv  2620  spc3gv  2622  ssoprab2  5484  bj-inf2vnlem1  7188