Theorem eqbrtrid 4123

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

Hypotheses

Ref	Expression
eqbrtrid.1	⊢ 𝐴 = 𝐵
eqbrtrid.2	⊢ (𝜑 → 𝐵𝑅𝐶)

Assertion

Ref	Expression
eqbrtrid	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem eqbrtrid

Step	Hyp	Ref	Expression
1		eqbrtrid.2	. 2 ⊢ (𝜑 → 𝐵𝑅𝐶)
2		eqbrtrid.1	. 2 ⊢ 𝐴 = 𝐵
3		eqid 2231	. 2 ⊢ 𝐶 = 𝐶
4	1, 2, 3	3brtr4g 4122	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1397   class class class wbr 4088

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-br 4089

This theorem is referenced by:  rex2dom  6995  xp1en  7006  caucvgprlemm  7887  intqfrac2  10580  m1modge3gt1  10632  bernneq2  10922  reccn2ap  11873  eirraplem  12337  nno  12466  bitsfzolem  12514  bitsinv1lem  12521  oddprmge3  12706  sqnprm  12707  4sqlem6  12955  4sqlem13m  12975  4sqlem16  12978  4sqlem17  12979  2expltfac  13011  oddennn  13012  strle2g  13189  strle3g  13190  1strstrg  13198  2strstrndx  13200  2strstrg  13201  rngstrg  13217  srngstrd  13228  lmodstrd  13246  ipsstrd  13258  topgrpstrd  13278  imasvalstrd  13352  znidom  14670  psmetge0  15054  reeff1olem  15494  cosq14gt0  15555  cosq34lt1  15573  ioocosf1o  15577  mersenne  15720  gausslemma2dlem0c  15779  gausslemma2dlem0e  15781  lgseisenlem1  15798  lgsquadlem1  15805  lgsquadlem2  15806  lgsquadlem3  15807  pwf1oexmid  16600  trilpolemeq1  16644