Theorem eqbrtrid 4163

Description: B chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)

Hypotheses

Ref	Expression
eqbrtrid.1	|- A = B
eqbrtrid.2	|- ( ph -> B R C )

Assertion

Ref	Expression
eqbrtrid	|- ( ph -> A R C )

Proof of Theorem eqbrtrid

Step	Hyp	Ref	Expression
1		eqbrtrid.2	. 2 |- ( ph -> B R C )
2		eqbrtrid.1	. 2 |- A = B
3		eqid 2238	. 2 |- C = C
4	1, 2, 3	3brtr4g 4162	1 |- ( ph -> A R C )

Syntax hints:   -> wi 4   = wceq 1402   class class class wbr 4128

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3714  df-pr 3715  df-op 3717  df-br 4129

This theorem is referenced by:  rex2dom  7103  xp1en  7114  caucvgprlemm  8028  intqfrac2  10737  m1modge3gt1  10789  bernneq2  11080  reccn2ap  12060  eirraplem  12525  nno  12654  bitsfzolem  12702  bitsinv1lem  12709  oddprmge3  12894  sqnprm  12895  4sqlem6  13143  4sqlem13m  13163  4sqlem16  13166  4sqlem17  13167  2expltfac  13199  oddennn  13264  strle2g  13441  strle3g  13442  1strstrg  13450  2strstrndx  13452  2strstrg  13453  rngstrg  13469  srngstrd  13480  lmodstrd  13498  ipsstrd  13510  topgrpstrd  13530  imasvalstrd  13599  znidom  14967  psmetge0  15358  reeff1olem  15798  cosq14gt0  15859  cosq34lt1  15877  ioocosf1o  15881  mersenne  16028  gausslemma2dlem0c  16087  gausslemma2dlem0e  16089  lgseisenlem1  16106  lgsquadlem1  16113  lgsquadlem2  16114  lgsquadlem3  16115  pwf1oexmid  16946  trilpolemeq1  16997