Theorem hbc 110

Description: Hypothesis builder for combination. (Contributed by Mario Carneiro, 8-Oct-2014.)

Hypotheses

Ref	Expression
hbc.1	⊢ F:(β → γ)
hbc.2	⊢ A:β
hbc.3	⊢ B:α
hbc.4	⊢ R⊧[(λx:α FB) = F]
hbc.5	⊢ R⊧[(λx:α AB) = A]

Assertion

Ref	Expression
hbc	⊢ R⊧[(λx:α (FA)B) = (FA)]

Proof of Theorem hbc

Step	Hyp	Ref	Expression
1		hbc.1	. . . . 5 ⊢ F:(β → γ)
2		hbc.2	. . . . 5 ⊢ A:β
3	1, 2	wc 50	. . . 4 ⊢ (FA):γ
4	3	wl 66	. . 3 ⊢ λx:α (FA):(α → γ)
5		hbc.3	. . 3 ⊢ B:α
6	4, 5	wc 50	. 2 ⊢ (λx:α (FA)B):γ
7		hbc.4	. . . 4 ⊢ R⊧[(λx:α FB) = F]
8	7	ax-cb1 29	. . 3 ⊢ R:∗
9	1, 2, 5	distrc 93	. . 3 ⊢ ⊤⊧[(λx:α (FA)B) = ((λx:α FB)(λx:α AB))]
10	8, 9	a1i 28	. 2 ⊢ R⊧[(λx:α (FA)B) = ((λx:α FB)(λx:α AB))]
11	1	wl 66	. . . 4 ⊢ λx:α F:(α → (β → γ))
12	11, 5	wc 50	. . 3 ⊢ (λx:α FB):(β → γ)
13		hbc.5	. . . 4 ⊢ R⊧[(λx:α AB) = A]
14	2, 13	eqtypri 81	. . 3 ⊢ (λx:α AB):β
15	12, 14, 7, 13	ceq12 88	. 2 ⊢ R⊧[((λx:α FB)(λx:α AB)) = (FA)]
16	6, 10, 15	eqtri 95	1 ⊢ R⊧[(λx:α (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-weq 40  ax-refl 42  ax-eqmp 45  ax-wc 49  ax-ceq 51  ax-wl 65  ax-distrc 68  ax-wov 71  ax-eqtypi 77  ax-eqtypri 80

This theorem depends on definitions:  df-ov 73

This theorem is referenced by:  hbov  111  clf  115  exlimdv  167  cbvf  179  leqf  181  exlimd  183  alimdv  184  eximdv  185  alnex  186  exmid  199  ax5  207  ax6  208  ax7  209  ax9  212  axext  219  axrep  220