Theorem eqtri 95

Description: Transitivity of equality. (Contributed by Mario Carneiro, 7-Oct-2014.)

Hypotheses

Ref	Expression
eqtri.1	⊢ A:α
eqtri.2	⊢ R⊧[A = B]
eqtri.3	⊢ R⊧[B = C]

Assertion

Ref	Expression
eqtri	⊢ R⊧[A = C]

Proof of Theorem eqtri

Step	Hyp	Ref	Expression
1		weq 41	. 2 ⊢ = :(α → (α → ∗))
2		eqtri.1	. 2 ⊢ A:α
3		eqtri.2	. . . 4 ⊢ R⊧[A = B]
4	2, 3	eqtypi 78	. . 3 ⊢ B:α
5		eqtri.3	. . 3 ⊢ R⊧[B = C]
6	4, 5	eqtypi 78	. 2 ⊢ C:α
7	1, 2, 4, 3	dfov1 74	. . 3 ⊢ R⊧(( = A)B)
8	1, 2	wc 50	. . . 4 ⊢ ( = A):(α → ∗)
9	8, 4, 5	ceq2 90	. . 3 ⊢ R⊧[(( = A)B) = (( = A)C)]
10	7, 9	mpbi 82	. 2 ⊢ R⊧(( = A)C)
11	1, 2, 6, 10	dfov2 75	1 ⊢ R⊧[A = C]

Syntax hints:   → ht 2  ∗hb 3  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

This theorem depends on definitions:  df-ov 73

This theorem is referenced by:  3eqtr4i  96  hbc  110  hbl  112  ovl  117  alval  142  exval  143  euval  144  notval  145  imval  146  orval  147  anval  148  ax4g  149  dfan2  154  ex  158  notval2  159  olc  164  orc  165  exlimdv  167  cbvf  179  exlimd  183  exmid  199  ax8  211  ax10  213  ax11  214  axrep  220  axpow  221  axun  222