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

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
StepHypRef Expression
1 weq 38 . 2 |- = :(al -> (al -> *))
2 eqtri.1 . 2 |- A:al
3 eqtri.2 . . . 4 |- R |= [A = B]
42, 3eqtypi 69 . . 3 |- B:al
5 eqtri.3 . . 3 |- R |= [B = C]
64, 5eqtypi 69 . 2 |- C:al
71, 2, 4, 3dfov1 66 . . 3 |- R |= (( = A)B)
81, 2wc 45 . . . 4 |- ( = A):(al -> *)
98, 4, 5ceq2 80 . . 3 |- R |= [(( = A)B) = (( = A)C)]
107, 9mpbi 72 . 2 |- R |= (( = A)C)
111, 2, 6, 10dfov2 67 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 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
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
  Copyright terms: Public domain W3C validator