Axiom ax-distrc 68

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

Hypotheses

Ref	Expression
ax-beta.1	|- A:be
ax-distrc.2	|- B:al
ax-distrc.3	|- F:(be -> ga)

Assertion

Ref	Expression
ax-distrc	|- T. |= (( = (\x:al (FA)B))((\x:al FB)(\x:al AB)))

Detailed syntax breakdown of Axiom ax-distrc

Step	Hyp	Ref	Expression
1		kt 8	. 2 term T.
2		ke 7	. . . 4 term =
3		hal	. . . . . 6 type al
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:al (FA)
9		tb	. . . . 5 term B
10	8, 9	kc 5	. . . 4 term (\x:al (FA)B)
11	2, 10	kc 5	. . 3 term ( = (\x:al (FA)B))
12	3, 4, 5	kl 6	. . . . 5 term \x:al F
13	12, 9	kc 5	. . . 4 term (\x:al FB)
14	3, 4, 6	kl 6	. . . . 5 term \x:al A
15	14, 9	kc 5	. . . 4 term (\x:al AB)
16	13, 15	kc 5	. . 3 term ((\x:al FB)(\x:al AB))
17	11, 16	kc 5	. 2 term (( = (\x:al (FA)B))((\x:al FB)(\x:al AB)))
18	1, 17	wffMMJ2 11	1 wff T. |= (( = (\x:al (FA)B))((\x:al FB)(\x:al AB)))

This axiom is referenced by:  distrc  93