Theorem oveq123 98

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

Hypotheses

Ref	Expression
oveq.1	⊢ F:(α → (β → γ))
oveq.2	⊢ A:α
oveq.3	⊢ B:β
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:(α → (β → γ))
2		oveq.2	. . . 4 ⊢ A:α
3	1, 2	wc 50	. . 3 ⊢ (FA):(β → γ)
4		oveq.3	. . 3 ⊢ B:β
5	3, 4	wc 50	. 2 ⊢ ((FA)B):γ
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 ⊢ = :(γ → (γ → ∗))
12	1, 2, 4	wov 72	. . 3 ⊢ [AFB]:γ
13	6	ax-cb1 29	. . . 4 ⊢ R:∗
14	1, 2, 4	df-ov 73	. . . 4 ⊢ ⊤⊧(( = [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:(α → (β → γ))
18	2, 7	eqtypi 78	. . . 4 ⊢ C:α
19	4, 9	eqtypi 78	. . . 4 ⊢ T:β
20	17, 18, 19	wov 72	. . 3 ⊢ [CST]:γ
21	17, 18	wc 50	. . . 4 ⊢ (SC):(β → γ)
22	21, 19	wc 50	. . 3 ⊢ ((SC)T):γ
23	17, 18, 19	df-ov 73	. . . 4 ⊢ ⊤⊧(( = [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]]

This proof depends on syntax axioms:   → ht 2  kc 5   = ke 7  [kbr 9  ⊧wffMMJ2 11  wffMMJ2t 12

This proof depends on 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 proof depends on definitions:  df-ov 73

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