Theorem eqtri 85

Description: Transitivity of equality.

Hypotheses

Ref	Expression
eqtri.1	|- A:al
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 38	. 2 |- = :(al -> (al -> *))
2		eqtri.1	. 2 |- A:al
3		eqtri.2	. . . 4 |- R |= [A = B]
4	2, 3	eqtypi 69	. . 3 |- B:al
5		eqtri.3	. . 3 |- R |= [B = C]
6	4, 5	eqtypi 69	. 2 |- C:al
7	1, 2, 4, 3	dfov1 66	. . 3 |- R |= (( = A)B)
8	1, 2	wc 45	. . . 4 |- ( = A):(al -> *)
9	8, 4, 5	ceq2 80	. . 3 |- R |= [(( = A)B) = (( = A)C)]
10	7, 9	mpbi 72	. 2 |- R |= (( = A)C)
11	1, 2, 6, 10	dfov2 67	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-refl 39  ax-eqmp 42  ax-ceq 46

This theorem depends on definitions:  df-ov 65

This theorem is referenced by:  3eqtr4i  86  hbc  100  hbl  102  ovl  107  alval  132  exval  133  euval  134  notval  135  imval  136  orval  137  anval  138  ax4g  139  dfan2  144  ex  148  notval2  149  olc  154  orc  155  exlimdv  157  cbvf  167  exlimd  171  exmid  186  ax8  198  ax10  200  ax11  201  axrep  207  axpow  208  axun  209