Theorem oveq123 98

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

Hypotheses

Ref	Expression
oveq.1	|- F:(al -> (be -> ga))
oveq.2	|- A:al
oveq.3	|- B:be
oveq123.4	|- R |= [F = S]
oveq123.5	|- R |= [A = C]
oveq123.6	|- R |= [B = T]

Assertion

Ref	Expression
oveq123	|- R |= [[AFB] = [CST]]

Proof of Theorem oveq123

Step	Hyp	Ref	Expression
1		oveq.1	. . . 4 |- F:(al -> (be -> ga))
2		oveq.2	. . . 4 |- A:al
3	1, 2	wc 50	. . 3 |- (FA):(be -> ga)
4		oveq.3	. . 3 |- B:be
5	3, 4	wc 50	. 2 |- ((FA)B):ga
6		oveq123.4	. . . 4 |- R |= [F = S]
7		oveq123.5	. . . 4 |- R |= [A = C]
8	1, 2, 6, 7	ceq12 88	. . 3 |- R |= [(FA) = (SC)]
9		oveq123.6	. . 3 |- R |= [B = T]
10	3, 4, 8, 9	ceq12 88	. 2 |- R |= [((FA)B) = ((SC)T)]
11		weq 41	. . 3 |- = :(ga -> (ga -> *))
12	1, 2, 4	wov 72	. . 3 |- [AFB]:ga
13	6	ax-cb1 29	. . . 4 |- R:*
14	1, 2, 4	df-ov 73	. . . 4 |- T. |= (( = [AFB])((FA)B))
15	13, 14	a1i 28	. . 3 |- R |= (( = [AFB])((FA)B))
16	11, 12, 5, 15	dfov2 75	. 2 |- R |= [[AFB] = ((FA)B)]
17	1, 6	eqtypi 78	. . . 4 |- S:(al -> (be -> ga))
18	2, 7	eqtypi 78	. . . 4 |- C:al
19	4, 9	eqtypi 78	. . . 4 |- T:be
20	17, 18, 19	wov 72	. . 3 |- [CST]:ga
21	17, 18	wc 50	. . . 4 |- (SC):(be -> ga)
22	21, 19	wc 50	. . 3 |- ((SC)T):ga
23	17, 18, 19	df-ov 73	. . . 4 |- T. |= (( = [CST])((SC)T))
24	13, 23	a1i 28	. . 3 |- R |= (( = [CST])((SC)T))
25	11, 20, 22, 24	dfov2 75	. 2 |- R |= [[CST] = ((SC)T)]
26	5, 10, 16, 25	3eqtr4i 96	1 |- R |= [[AFB] = [CST]]

Syntax hints:   -> ht 2  kc 5   = 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-wov 71  ax-eqtypi 77  ax-eqtypri 80

This theorem depends on definitions:  df-ov 73

This theorem is referenced by:  oveq1  99  oveq12  100  oveq  102