Theorem eqbrtrid 4128

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 4127	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1398   class class class wbr 4093

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-br 4094

This theorem is referenced by:  rex2dom  7039  xp1en  7050  caucvgprlemm  7931  intqfrac2  10627  m1modge3gt1  10679  bernneq2  10969  reccn2ap  11936  eirraplem  12401  nno  12530  bitsfzolem  12578  bitsinv1lem  12585  oddprmge3  12770  sqnprm  12771  4sqlem6  13019  4sqlem13m  13039  4sqlem16  13042  4sqlem17  13043  2expltfac  13075  oddennn  13076  strle2g  13253  strle3g  13254  1strstrg  13262  2strstrndx  13264  2strstrg  13265  rngstrg  13281  srngstrd  13292  lmodstrd  13310  ipsstrd  13322  topgrpstrd  13342  imasvalstrd  13416  znidom  14736  psmetge0  15125  reeff1olem  15565  cosq14gt0  15626  cosq34lt1  15644  ioocosf1o  15648  mersenne  15794  gausslemma2dlem0c  15853  gausslemma2dlem0e  15855  lgseisenlem1  15872  lgsquadlem1  15879  lgsquadlem2  15880  lgsquadlem3  15881  pwf1oexmid  16704  trilpolemeq1  16755