HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  eqtri Unicode version

Theorem eqtri 95
Description: Transitivity of equality. (Contributed by Mario Carneiro, 7-Oct-2014.)
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
StepHypRef Expression
1 weq 41 . 2 |- = :(al -> (al -> *))
2 eqtri.1 . 2 |- A:al
3 eqtri.2 . . . 4 |- R |= [A = B]
42, 3eqtypi 78 . . 3 |- B:al
5 eqtri.3 . . 3 |- R |= [B = C]
64, 5eqtypi 78 . 2 |- C:al
71, 2, 4, 3dfov1 74 . . 3 |- R |= (( = A)B)
81, 2wc 50 . . . 4 |- ( = A):(al -> *)
98, 4, 5ceq2 90 . . 3 |- R |= [(( = A)B) = (( = A)C)]
107, 9mpbi 82 . 2 |- R |= (( = A)C)
111, 2, 6, 10dfov2 75 1 |- R |= [A = C]
Colors of variables: type var term
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
  Copyright terms: Public domain W3C validator