Theorem eqbrtrid 4060

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 2189	. 2 |- C = C
4	1, 2, 3	3brtr4g 4059	1 |- ( ph -> A R C )

Syntax hints:   -> wi 4   = wceq 1364   class class class wbr 4025

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2758  df-un 3152  df-sn 3620  df-pr 3621  df-op 3623  df-br 4026

This theorem is referenced by:  xp1en  6857  caucvgprlemm  7707  intqfrac2  10362  m1modge3gt1  10414  bernneq2  10688  reccn2ap  11368  eirraplem  11831  nno  11958  oddprmge3  12184  sqnprm  12185  4sqlem6  12432  4sqlem13m  12452  4sqlem16  12455  4sqlem17  12456  oddennn  12460  strle2g  12636  strle3g  12637  1strstrg  12645  2strstrg  12647  rngstrg  12663  srngstrd  12674  lmodstrd  12692  ipsstrd  12704  topgrpstrd  12724  psmetge0  14352  reeff1olem  14730  cosq14gt0  14791  cosq34lt1  14809  ioocosf1o  14813  lgseisenlem1  14989  pwf1oexmid  15289  trilpolemeq1  15329