Theorem hbald 1109

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

Hypotheses

Ref	Expression
hbald.1	|- (ph -> A.yph)
hbald.2	|- (ph -> (ps -> A.xps))

Assertion

Ref	Expression
hbald	|- (ph -> (A.yps -> A.xA.yps))

Proof of Theorem hbald

Step	Hyp	Ref	Expression
1		hbald.1	. . 3 |- (ph -> A.yph)
2		hbald.2	. . 3 |- (ph -> (ps -> A.xps))
3	1, 2	19.20d 993	. 2 |- (ph -> (A.yps -> A.yA.xps))
4		ax-7 959	. 2 |- (A.yA.xps -> A.xA.yps)
5	3, 4	syl6 22	1 |- (ph -> (A.yps -> A.xA.yps))

Syntax hints:   -> wi 3  A.wal 951

This theorem is referenced by:  dvelimfALT 1149  hbeu 1382  ralcom2 1768  axrepndlem2 4917  axunnd 4920  axpowndlem2 4922  axpowndlem4 4924  axregndlem2 4927  axinfndlem1 4929  axinfnd 4930  axacndlem4 4934  axacndlem5 4935  axacnd 4936

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-7 959  ax-gen 960  ax-4 970  ax-5o 972

Copyright terms: Public domain