Theorem hbc 100

Description: Hypothesis builder for combination.

Hypotheses

Ref	Expression
hbc.1	|- F:(be -> ga)
hbc.2	|- A:be
hbc.3	|- B:al
hbc.4	|- R |= [(\x:al FB) = F]
hbc.5	|- R |= [(\x:al AB) = A]

Assertion

Ref	Expression
hbc	|- R |= [(\x:al (FA)B) = (FA)]

Proof of Theorem hbc

Step	Hyp	Ref	Expression
1		hbc.1	. . . . 5 |- F:(be -> ga)
2		hbc.2	. . . . 5 |- A:be
3	1, 2	wc 45	. . . 4 |- (FA):ga
4	3	wl 59	. . 3 |- \x:al (FA):(al -> ga)
5		hbc.3	. . 3 |- B:al
6	4, 5	wc 45	. 2 |- (\x:al (FA)B):ga
7		hbc.4	. . . 4 |- R |= [(\x:al FB) = F]
8	7	ax-cb1 29	. . 3 |- R:*
9	1, 2, 5	distrc 83	. . 3 |- T. |= [(\x:al (FA)B) = ((\x:al FB)(\x:al AB))]
10	8, 9	a1i 28	. 2 |- R |= [(\x:al (FA)B) = ((\x:al FB)(\x:al AB))]
11	1	wl 59	. . . 4 |- \x:al F:(al -> (be -> ga))
12	11, 5	wc 45	. . 3 |- (\x:al FB):(be -> ga)
13		hbc.5	. . . 4 |- R |= [(\x:al AB) = A]
14	2, 13	eqtypri 71	. . 3 |- (\x:al AB):be
15	12, 14, 7, 13	ceq12 78	. 2 |- R |= [((\x:al FB)(\x:al AB)) = (FA)]
16	6, 10, 15	eqtri 85	1 |- R |= [(\x:al (FA)B) = (FA)]

Syntax hints:   -> ht 2  kc 5  \kl 6   = ke 7  [kbr 9   |= wffMMJ2 11  wffMMJ2t 12

This theorem was proved from axioms:  ax-syl 15  ax-jca 17  ax-trud 26  ax-cb1 29  ax-cb2 30  ax-refl 39  ax-eqmp 42  ax-ceq 46  ax-distrc 61

This theorem depends on definitions:  df-ov 65

This theorem is referenced by:  hbov  101  clf  105  exlimdv  157  cbvf  167  leqf  169  exlimd  171  alimdv  172  eximdv  173  alnex  174  exmid  186  ax5  194  ax6  195  ax7  196  ax9  199  axext  206  axrep  207