Theorem hbexd 1116

Description: Deduction form of bound-variable hypothesis builder hbex 1008.

Hypotheses

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

Assertion

Ref	Expression
hbexd	|- (ph -> (E.yps -> A.xE.yps))

Proof of Theorem hbexd

Step	Hyp	Ref	Expression
1		hbexd.1	. . 3 |- (ph -> A.yph)
2		hbexd.2	. . 3 |- (ph -> (ps -> A.xps))
3	1, 2	19.22d 1064	. 2 |- (ph -> (E.yps -> E.yA.xps))
4		19.12 1049	. 2 |- (E.yA.xps -> A.xE.yps)
5	3, 4	syl6 22	1 |- (ph -> (E.yps -> A.xE.yps))

Syntax hints:   -> wi 3  A.wal 956  E.wex 982

This theorem is referenced by:  axrepndlem1 4956  axrepndlem2 4957  axunndlem1 4959  axunnd 4960  axpowndlem2 4962  axpowndlem3 4963  axpowndlem4 4964  axregndlem2 4967  axinfndlem1 4969  axinfnd 4970  axacndlem4 4974  axacndlem5 4975  axacnd 4976

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-4 975  ax-5o 977  ax-6o 980

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983

Copyright terms: Public domain