Theorem hbald 1145

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

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 1028	. 2 |- (ph -> (A.yps -> A.yA.xps))
4		ax-7 994	. 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 986

This theorem is referenced by:  dvelimfALT 1186  dvelimALT 1386  hbeu 1422  ralcom2 1814  axrepndlem2 5034  axunnd 5037  axpowndlem2 5039  axpowndlem4 5041  axregndlem2 5044  axinfndlem1 5046  axinfnd 5047  axacndlem4 5051  axacndlem5 5052  axacnd 5053

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-7 994  ax-gen 995  ax-4 1005  ax-5o 1007

Copyright terms: Public domain