Axiom ax-distrc 68

Description: Distribution of combination over substitution. (Contributed by Mario Carneiro, 8-Oct-2014.)

Hypotheses

Ref	Expression
ax-beta.1	⊢ A:β
ax-distrc.2	⊢ B:α
ax-distrc.3	⊢ F:(β → γ)

Assertion

Ref	Expression
ax-distrc	⊢ ⊤⊧(( = (λx:α (FA)B))((λx:α FB)(λx:α AB)))

Detailed syntax breakdown of Axiom ax-distrc

Step	Hyp	Ref	Expression
1		kt 8	. 2 term ⊤
2		ke 7	. . . 4 term =
3		hal	. . . . . 6 type α
4		vx	. . . . . 6 var x
5		tf	. . . . . . 7 term F
6		ta	. . . . . . 7 term A
7	5, 6	kc 5	. . . . . 6 term (FA)
8	3, 4, 7	kl 6	. . . . 5 term λx:α (FA)
9		tb	. . . . 5 term B
10	8, 9	kc 5	. . . 4 term (λx:α (FA)B)
11	2, 10	kc 5	. . 3 term ( = (λx:α (FA)B))
12	3, 4, 5	kl 6	. . . . 5 term λx:α F
13	12, 9	kc 5	. . . 4 term (λx:α FB)
14	3, 4, 6	kl 6	. . . . 5 term λx:α A
15	14, 9	kc 5	. . . 4 term (λx:α AB)
16	13, 15	kc 5	. . 3 term ((λx:α FB)(λx:α AB))
17	11, 16	kc 5	. 2 term (( = (λx:α (FA)B))((λx:α FB)(λx:α AB)))
18	1, 17	wffMMJ2 11	1 wff ⊤⊧(( = (λx:α (FA)B))((λx:α FB)(λx:α AB)))

This axiom is referenced by:  distrc  93