Theorem hbimd 787

Description: Deduction form of bound-variable hypothesis builder hbim 702.

Hypotheses

Ref	Expression
hbimd.1	|- (ph -> A.xph)
hbimd.2	|- (ph -> (ps -> A.xps))
hbimd.3	|- (ph -> (ch -> A.xch))

Assertion

Ref	Expression
hbimd	|- (ph -> ((ps -> ch) -> A.x(ps -> ch)))

Proof of Theorem hbimd

Step	Hyp	Ref	Expression
1		hbimd.1	. . . . . 6 |- (ph -> A.xph)
2		hbimd.2	. . . . . 6 |- (ph -> (ps -> A.xps))
3	1, 2	hbnd 786	. . . . 5 |- (ph -> (-. ps -> A.x -. ps))
4	3	com12 13	. . . 4 |- (-. ps -> (ph -> A.x -. ps))
5		pm2.21 71	. . . . 5 |- (-. ps -> (ps -> ch))
6	5	19.20i 691	. . . 4 |- (A.x -. ps -> A.x(ps -> ch))
7	4, 6	syl6 23	. . 3 |- (-. ps -> (ph -> A.x(ps -> ch)))
8		hbimd.3	. . . . 5 |- (ph -> (ch -> A.xch))
9	8	com12 13	. . . 4 |- (ch -> (ph -> A.xch))
10		ax-1 3	. . . . 5 |- (ch -> (ps -> ch))
11	10	19.20i 691	. . . 4 |- (A.xch -> A.x(ps -> ch))
12	9, 11	syl6 23	. . 3 |- (ch -> (ph -> A.x(ps -> ch)))
13	7, 12	ja 118	. 2 |- ((ps -> ch) -> (ph -> A.x(ps -> ch)))
14	13	com12 13	1 |- (ph -> ((ps -> ch) -> A.x(ps -> ch)))

Syntax hints:  -. wn 1   -> wi 2  A.wal 672

This theorem is referenced by:  hbbid 789  19.21g 792  hbsb4 905  ddelimf2 907  ralcom2 1314  axrepndlem1 3738  axrepndlem2 3739  axunndlem1 3741  axunnd 3742  axpowndlem2 3744  axpowndlem3 3745  axpowndlem4 3746  axregndlem2 3749  axregnd 3750  axinfndlem1 3751  axinfnd 3752  axacndlem4 3756  axacndlem5 3757  axacnd 3758

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677

metamath.org