Theorem eqbrtrd 4115

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 8-Oct-1999.)

Hypotheses

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

Assertion

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

Proof of Theorem eqbrtrd

Step	Hyp	Ref	Expression
1		eqbrtrd.2	. 2 |- ( ph -> B R C )
2		eqbrtrd.1	. . 3 |- ( ph -> A = B )
3	2	breq1d 4103	. 2 |- ( ph -> ( A R C <-> B R C ) )
4	1, 3	mpbird 167	1 |- ( ph -> A R C )

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:  eqbrtrrd  4117  dif1en  7111  ccfunen  7543  prarloclemcalc  7782  ltexprlemopu  7883  recexprlemloc  7911  caucvgprprlemloccalc  7964  suplocsrlem  8088  axpre-suploclemres  8181  mulle0r  9183  lbinfle  9189  divge1  10019  xltnegi  10131  xleadd1a  10169  xltadd1  10172  xlt2add  10176  xposdif  10178  xleaddadd  10183  lincmble  10300  ubmelm1fzo  10534  zsupssdc  10561  qbtwnrelemcalc  10578  qbtwnxr  10580  ceiqm1l  10636  ceilqm1lt  10637  ceilqle  10639  modqlt  10658  modqeqmodmin  10719  addmodlteq  10723  seqf1oglem1  10844  exp3vallem  10865  bernneq  10985  nn0ltexp2  11034  faclbnd2  11067  ccatsymb  11245  ccatrn  11252  resqrexlemdec  11651  resqrexlemcalc2  11655  resqrexlemglsq  11662  resqrexlemga  11663  abslt  11728  amgm2  11758  icodiamlt  11820  maxabsle  11844  maxltsup  11858  minmax  11870  min1inf  11872  min2inf  11873  bdtrilem  11879  xrmaxltsup  11898  xrmaxaddlem  11900  xrmaxadd  11901  xrminmax  11905  xrmin1inf  11907  xrmin2inf  11908  climconst  11930  serclim0  11945  mulcn2  11952  reccn2ap  11953  iserex  11979  climlec2  11981  iserge0  11983  climcau  11987  climcvg1nlem  11989  fsumabs  12106  iserabs  12116  isumlessdc  12137  divcnv  12138  expcnvre  12144  absgtap  12151  georeclim  12154  cvgratnnlembern  12164  cvgratnnlemsumlt  12169  cvgratnnlemfm  12170  cvgratnnlemrate  12171  mertenslemub  12175  mertenslemi1  12176  prodfclim1  12185  prodfap0  12186  efcvgfsum  12308  eftlub  12331  eflegeo  12342  tanval3ap  12355  tannegap  12369  ef01bndlem  12397  sin01bnd  12398  cos01bnd  12399  cos01gt0  12404  bitsfzolem  12595  bitsfzo  12596  bitsinv1lem  12602  mulgcd  12667  nnminle  12686  eucalglt  12709  lcmledvds  12722  mulgcddvds  12746  prmind2  12772  isprm5lem  12793  pw2dvdslemn  12817  pw2dvdseulemle  12819  oddpwdclemdvds  12822  sqrt2irrap  12832  divdenle  12849  nonsq  12859  pythagtriplem4  12921  pclem0  12939  pcpremul  12946  pczdvds  12967  pcprmpw2  12986  qexpz  13005  4sqlem10  13040  ennnfonelemkh  13113  prdsbaslemss  13437  triv1nsgd  13885  qusgrp  13899  gsumsplit0  14013  bl2in  15214  xblcntrps  15224  xblcntr  15225  ssblps  15236  ssbl  15237  blssps  15238  blss  15239  xmetxp  15318  mulc1cncf  15400  cncfmptc  15407  mulcncflem  15418  ivthinclemlopn  15447  ivthinclemuopn  15449  ivthdec  15455  ivthreinc  15456  hovera  15458  hoverlt1  15460  limcimolemlt  15475  cnplimclemle  15479  cnplimclemr  15480  limccnp2lem  15487  dveflem  15537  reeff1olem  15582  reeff1oleme  15583  tangtx  15649  cosq34lt1  15661  logdivlti  15692  cxpap0  15715  rpabscxpbnd  15751  pellexlem2  15792  mersenne  15811  lgslem3  15821  gausslemma2dlem1a  15877  lgsquadlem1  15896  lgsquadlem2  15897  2lgslem1c  15909  subumgredg2en  16212  qdencn  16755  cvgcmp2nlemabs  16764  trilpolemclim  16768  trilpolemisumle  16770  trilpolemeq1  16772  apdifflemf  16778  apdifflemr  16779