ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqbrtrrid GIF version

Theorem eqbrtrrid 4013
Description: B chained equality inference for a binary relation. (Contributed by NM, 17-Sep-2004.)
Hypotheses
Ref Expression
eqbrtrrid.1 𝐵 = 𝐴
eqbrtrrid.2 (𝜑𝐵𝑅𝐶)
Assertion
Ref Expression
eqbrtrrid (𝜑𝐴𝑅𝐶)

Proof of Theorem eqbrtrrid
StepHypRef Expression
1 eqbrtrrid.2 . 2 (𝜑𝐵𝑅𝐶)
2 eqbrtrrid.1 . 2 𝐵 = 𝐴
3 eqid 2164 . 2 𝐶 = 𝐶
41, 2, 33brtr3g 4010 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1342   class class class wbr 3977
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146
This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-v 2724  df-un 3116  df-sn 3577  df-pr 3578  df-op 3580  df-br 3978
This theorem is referenced by:  enpr1g  6756  endjudisj  7158  recexprlem1ssl  7566  addgt0  8338  addgegt0  8339  addgtge0  8340  addge0  8341  expge1  10483  expcnv  11435  fprodge1  11570  cos12dec  11698  ncoprmgcdne1b  12010  phicl2  12135  exmidunben  12322  sin0pilem2  13270  cosq23lt0  13321  cos0pilt1  13340  rplogcl  13367  logge0  13368  logdivlti  13369
  Copyright terms: Public domain W3C validator