Theorem hbald 790

Description: Deduction form of bound-variable hypothesis builder hbal 700.

Hypotheses

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

Assertion

Ref	Expression
hbald	⊢ (φ → (∀yψ → ∀x∀yψ))

Proof of Theorem hbald

Step	Hyp	Ref	Expression
1		hbald.1	. . 3 ⊢ (φ → ∀yφ)
2		hbald.2	. . 3 ⊢ (φ → (ψ → ∀xψ))
3	1, 2	19.20d 693	. 2 ⊢ (φ → (∀yψ → ∀y∀xψ))
4		ax-7 676	. 2 ⊢ (∀y∀xψ → ∀x∀yψ)
5	3, 4	syl6 23	1 ⊢ (φ → (∀yψ → ∀x∀yψ))

Syntax hints:   → wi 2  ∀wal 672

This theorem is referenced by:  ddelimf2 907  hbeu 1016  ralcom2 1314  axrepndlem2 3739  axunnd 3742  axpowndlem2 3744  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-mp 6  ax-4 673  ax-5 674  ax-7 676  ax-gen 677

metamath.org