Theorem hbald 1112

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

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 995	. 2 |- (ph -> (A.yps -> A.yA.xps))
4		ax-7 961	. 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 953

This theorem is referenced by:  dvelimfALT 1152  dvelimALT 1352  hbeu 1388  ralcom2 1774  axrepndlem2 4928  axunnd 4931  axpowndlem2 4933  axpowndlem4 4935  axregndlem2 4938  axinfndlem1 4940  axinfnd 4941  axacndlem4 4945  axacndlem5 4946  axacnd 4947

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-7 961  ax-gen 962  ax-4 972  ax-5o 974

Copyright terms: Public domain