Theorem eqbrtrd 4136

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 4124	. 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 4114

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 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703  df-br 4115

This theorem is referenced by:  eqbrtrrd  4138  dif1en  7149  ccfunen  7594  prarloclemcalc  7833  ltexprlemopu  7934  recexprlemloc  7962  caucvgprprlemloccalc  8015  suplocsrlem  8139  axpre-suploclemres  8232  mulle0r  9235  lbinfle  9241  divge1  10074  ltesubnnd  10120  xltnegi  10187  xleadd1a  10225  xltadd1  10228  xlt2add  10232  xposdif  10234  xleaddadd  10239  lincmble  10356  ubmelm1fzo  10593  infssfzledc  10619  zsupssdc  10622  qbtwnrelemcalc  10639  qbtwnxr  10641  ceiqm1l  10697  ceilqm1lt  10698  ceilqle  10700  modqlt  10719  modqeqmodmin  10780  addmodlteq  10784  seqf1oglem1  10905  exp3vallem  10926  bernneq  11047  nn0ltexp2  11096  faclbnd2  11129  sshashneg  11230  ccatsymb  11315  ccatrn  11322  resqrexlemdec  11721  resqrexlemcalc2  11725  resqrexlemglsq  11732  resqrexlemga  11733  abslt  11798  amgm2  11828  icodiamlt  11890  maxabsle  11914  maxltsup  11928  minmax  11940  min1inf  11942  min2inf  11943  bdtrilem  11949  xrmaxltsup  11968  xrmaxaddlem  11970  xrmaxadd  11971  xrminmax  11975  xrmin1inf  11977  xrmin2inf  11978  climconst  12000  serclim0  12015  mulcn2  12022  reccn2ap  12023  iserex  12049  climlec2  12051  iserge0  12053  climcau  12057  climcvg1nlem  12059  fsumabs  12176  iserabs  12186  isumlessdc  12207  divcnv  12208  expcnvre  12214  absgtap  12221  georeclim  12224  cvgratnnlembern  12234  cvgratnnlemsumlt  12239  cvgratnnlemfm  12240  cvgratnnlemrate  12241  mertenslemub  12245  mertenslemi1  12246  prodfclim1  12255  prodfap0  12256  efcvgfsum  12378  eftlub  12401  eflegeo  12412  tanval3ap  12425  tannegap  12439  ef01bndlem  12467  sin01bnd  12468  cos01bnd  12469  cos01gt0  12474  bitsfzolem  12665  bitsfzo  12666  bitsinv1lem  12672  mulgcd  12737  nnminle  12756  eucalglt  12779  lcmledvds  12792  mulgcddvds  12816  prmind2  12842  isprm5lem  12863  pw2dvdslemn  12887  pw2dvdseulemle  12889  oddpwdclemdvds  12892  sqrt2irrap  12902  divdenle  12919  nonsq  12929  pythagtriplem4  12991  pclem0  13009  pcpremul  13016  pczdvds  13037  pcprmpw2  13056  qexpz  13075  4sqlem10  13110  ballotfilemimin  13193  ballotfilemsel1i  13200  ballotfilemro  13210  ennnfonelemkh  13247  triv1nsgd  13971  qusgrp  13985  gsumsplit0  14099  prdsbaslemss  14116  bl2in  15394  xblcntrps  15404  xblcntr  15405  ssblps  15416  ssbl  15417  blssps  15418  blss  15419  xmetxp  15498  mulc1cncf  15580  cncfmptc  15587  mulcncflem  15598  ivthinclemlopn  15627  ivthinclemuopn  15629  ivthdec  15635  ivthreinc  15636  hovera  15638  hoverlt1  15640  limcimolemlt  15655  cnplimclemle  15659  cnplimclemr  15660  limccnp2lem  15667  dveflem  15717  reeff1olem  15762  reeff1oleme  15763  tangtx  15829  cosq34lt1  15841  logdivlti  15872  cxpap0  15895  rpabscxpbnd  15931  pellexlem2  15972  mersenne  15991  lgslem3  16001  gausslemma2dlem1a  16057  lgsquadlem1  16076  lgsquadlem2  16077  2lgslem1c  16089  subumgredg2en  16392  qdencn  16933  cvgcmp2nlemabs  16942  trilpolemclim  16946  trilpolemisumle  16948  trilpolemeq1  16950  apdifflemf  16956  apdifflemr  16957