Theorem hbexd 1110

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

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 1058	. 2 |- (ph -> (E.yps -> E.yA.xps))
4		19.12 1043	. 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 951  E.wex 977

This theorem is referenced by:  axrepndlem1 4916  axrepndlem2 4917  axunndlem1 4919  axunnd 4920  axpowndlem2 4922  axpowndlem3 4923  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-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-4 970  ax-5o 972  ax-6o 975

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

Copyright terms: Public domain