Axiom ax-ceq 51

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

Hypotheses

Ref	Expression
ax-ceq.1	⊢ F:(α → β)
ax-ceq.2	⊢ T:(α → β)
ax-ceq.3	⊢ A:α
ax-ceq.4	⊢ B:α

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