Theorem hbald 1113

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

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 996	. 2 |- (ph -> (A.yps -> A.yA.xps))
4		ax-7 962	. 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 954

This theorem is referenced by:  dvelimfALT 1153  dvelimALT 1353  hbeu 1389  ralcom2 1776  axrepndlem2 4945  axunnd 4948  axpowndlem2 4950  axpowndlem4 4952  axregndlem2 4955  axinfndlem1 4957  axinfnd 4958  axacndlem4 4962  axacndlem5 4963  axacnd 4964

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-7 962  ax-gen 963  ax-4 973  ax-5o 975

Copyright terms: Public domain