Theorem hbimd 1106

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

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	. . . . 5 |- (ph -> A.xph)
2		hbimd.2	. . . . 5 |- (ph -> (ps -> A.xps))
3	1, 2	hbnd 1105	. . . 4 |- (ph -> (-. ps -> A.x -. ps))
4		pm2.21 76	. . . . 5 |- (-. ps -> (ps -> ch))
5	4	19.20i 989	. . . 4 |- (A.x -. ps -> A.x(ps -> ch))
6	3, 5	syl6com 53	. . 3 |- (-. ps -> (ph -> A.x(ps -> ch)))
7		hbimd.3	. . . 4 |- (ph -> (ch -> A.xch))
8		ax-1 4	. . . . 5 |- (ch -> (ps -> ch))
9	8	19.20i 989	. . . 4 |- (A.xch -> A.x(ps -> ch))
10	7, 9	syl6com 53	. . 3 |- (ch -> (ph -> A.x(ps -> ch)))
11	6, 10	ja 137	. 2 |- ((ps -> ch) -> (ph -> A.x(ps -> ch)))
12	11	com12 11	1 |- (ph -> ((ps -> ch) -> A.x(ps -> ch)))

Syntax hints:  -. wn 2   -> wi 3  A.wal 951

This theorem is referenced by:  hbbid 1108  19.21t 1111  dvelimfALT 1149  hbsb4 1243  a12lem1 1369  ralcom2 1768  reuuni2f 2873  axrepndlem1 4916  axrepndlem2 4917  axunndlem1 4919  axunnd 4920  axpowndlem2 4922  axpowndlem3 4923  axpowndlem4 4924  axregndlem2 4927  axregnd 4928  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-gen 960  ax-4 970  ax-5o 972  ax-6o 975

Copyright terms: Public domain