Theorem hbimd 1086

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

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 1085	. . . 4 |- (ph -> (-. ps -> A.x -. ps))
4		pm2.21 76	. . . . 5 |- (-. ps -> (ps -> ch))
5	4	19.20i 968	. . . 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 968	. . . 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 950

This theorem is referenced by:  hbbid 1088  19.21t 1091  dvelimfALT 1136  hbsb4 1232  a12lem1 1353  ralcom2 1752  reuuni2f 2846  axrepndlem1 4867  axrepndlem2 4868  axunndlem1 4870  axunnd 4871  axpowndlem2 4873  axpowndlem3 4874  axpowndlem4 4875  axregndlem2 4878  axregnd 4879  axinfndlem1 4880  axinfnd 4881  axacndlem4 4885  axacndlem5 4886  axacnd 4887

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-gen 955

Copyright terms: Public domain