Axiom ax-ceq 51

Description: Equality theorem for combination. (Contributed by Mario Carneiro, 7-Oct-2014.)

Hypotheses

Ref	Expression
ax-ceq.1	|- F:(al -> be)
ax-ceq.2	|- T:(al -> be)
ax-ceq.3	|- A:al
ax-ceq.4	|- B:al

Assertion

Ref	Expression
ax-ceq	|- ((( = F)T), (( = A)B)) |= (( = (FA))(TB))

Detailed syntax breakdown of Axiom ax-ceq

Step	Hyp	Ref	Expression
1		ke 7	. . . . 5 term =
2		tf	. . . . 5 term F
3	1, 2	kc 5	. . . 4 term ( = F)
4		tt	. . . 4 term T
5	3, 4	kc 5	. . 3 term (( = F)T)
6		ta	. . . . 5 term A
7	1, 6	kc 5	. . . 4 term ( = A)
8		tb	. . . 4 term B
9	7, 8	kc 5	. . 3 term (( = A)B)
10	5, 9	kct 10	. 2 term ((( = F)T), (( = A)B))
11	2, 6	kc 5	. . . 4 term (FA)
12	1, 11	kc 5	. . 3 term ( = (FA))
13	4, 8	kc 5	. . 3 term (TB)
14	12, 13	kc 5	. 2 term (( = (FA))(TB))
15	10, 14	wffMMJ2 11	1 wff ((( = F)T), (( = A)B)) |= (( = (FA))(TB))

This axiom is referenced by:  eqcomx  52  ceq12  88