Theorem hbexd 791

Description: Deduction form of bound-variable hypothesis builder hbex 701.

Hypotheses

Ref	Expression
hbexd.1	⊢ (φ → ∀yφ)
hbexd.2	⊢ (φ → (ψ → ∀xψ))

Assertion

Ref	Expression
hbexd	⊢ (φ → (∃yψ → ∀x∃yψ))

Proof of Theorem hbexd

Step	Hyp	Ref	Expression
1		hbexd.1	. . 3 ⊢ (φ → ∀yφ)
2		hbexd.2	. . 3 ⊢ (φ → (ψ → ∀xψ))
3	1, 2	19.22d 744	. 2 ⊢ (φ → (∃yψ → ∃y∀xψ))
4		19.12 729	. 2 ⊢ (∃y∀xψ → ∀x∃yψ)
5	3, 4	syl6 23	1 ⊢ (φ → (∃yψ → ∀x∃yψ))

Syntax hints:   → wi 2  ∀wal 672  ∃wex 678

This theorem is referenced by:  axrepndlem1 3738  axrepndlem2 3739  axunndlem1 3741  axunnd 3742  axpowndlem2 3744  axpowndlem3 3745  axpowndlem4 3746  axregndlem2 3749  axinfndlem1 3751  axinfnd 3752  axacndlem4 3756  axacndlem5 3757  axacnd 3758

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679

metamath.org