Theorem hbnd 786

Description: A deduction form of bound-variable hypothesis builder hbne 699.

Hypotheses

Ref	Expression
hbnd.1	|- (ph -> A.xph)
hbnd.2	|- (ph -> (ps -> A.xps))

Assertion

Ref	Expression
hbnd	|- (ph -> (-. ps -> A.x -. ps))

Proof of Theorem hbnd

Step	Hyp	Ref	Expression
1		hbnd.1	. . 3 |- (ph -> A.xph)
2		hbnd.2	. . 3 |- (ph -> (ps -> A.xps))
3	1, 2	19.21ai 740	. 2 |- (ph -> A.x(ps -> A.xps))
4		hbnt 710	. 2 |- (A.x(ps -> A.xps) -> (-. ps -> A.x -. ps))
5	3, 4	syl 12	1 |- (ph -> (-. ps -> A.x -. ps))

Syntax hints:  -. wn 1   -> wi 2  A.wal 672

This theorem is referenced by:  hbimd 787  cbvexd 978  axpowndlem2 3744  axpowndlem3 3745  axpowndlem4 3746  axregndlem2 3749  axregnd 3750

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-gen 677

metamath.org