Theorem eqbrtrd 4152

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 4140	. 2 |- ( ph -> ( A R C <-> B R C ) )
4	1, 3	mpbird 167	1 |- ( ph -> A R C )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   class class class wbr 4130

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-br 4131

This theorem is used by:  eqbrtrrd  4154  dif1en  7183  ccfunen  7630  prarloclemcalc  7869  ltexprlemopu  7970  recexprlemloc  7998  caucvgprprlemloccalc  8051  suplocsrlem  8175  axpre-suploclemres  8268  lesub3d  8892  mulle0r  9276  lbinfle  9282  divge1  10134  ltesubnnd  10180  xltnegi  10247  xleadd1a  10285  xltadd1  10288  xlt2add  10292  xposdif  10294  xleaddadd  10299  lincmble  10416  ubmelm1fzo  10654  infssfzledc  10680  zsupssdc  10683  qbtwnrelemcalc  10700  qbtwnxr  10702  ceiqm1l  10761  ceilqm1lt  10762  ceilqle  10764  modqlt  10783  modqeqmodmin  10844  addmodlteq  10848  seqf1oglem1  10969  exp3vallem  10990  bernneq  11111  nn0ltexp2  11161  faclbnd2  11194  sshashneg  11295  ccatsymb  11384  ccatrn  11391  sq01  11674  resqrexlemdec  11791  resqrexlemcalc2  11795  resqrexlemglsq  11802  resqrexlemga  11803  abslt  11869  amgm2  11899  icodiamlt  11961  maxabsle  11985  maxltsup  11999  minmax  12011  min1inf  12013  min2inf  12014  bdtrilem  12021  xrmaxltsup  12040  xrmaxaddlem  12042  xrmaxadd  12043  xrminmax  12047  xrmin1inf  12049  xrmin2inf  12050  climconst  12072  serclim0  12087  mulcn2  12094  reccn2ap  12095  iserex  12121  climlec2  12123  iserge0  12125  climcau  12129  climcvg1nlem  12131  fsumabs  12248  iserabs  12258  isumlessdc  12279  divcnv  12280  expcnvre  12286  absgtap  12293  georeclim  12296  cvgratnnlembern  12306  cvgratnnlemsumlt  12311  cvgratnnlemfm  12312  cvgratnnlemrate  12313  mertenslemub  12317  mertenslemi1  12318  prodfclim1  12327  prodfap0  12328  efcvgfsum  12450  eftlub  12473  eflegeo  12484  tanval3ap  12497  tannegap  12511  ef01bndlem  12539  sin01bnd  12540  cos01bnd  12541  cos01gt0  12546  bitsfzolem  12737  bitsfzo  12738  bitsinv1lem  12744  mulgcd  12809  nnminle  12828  eucalglt  12851  lcmledvds  12864  mulgcddvds  12888  prmind2  12914  isprm5lem  12936  pwbdvdslemn  12960  pwbdvdseulemle  12962  nnmaxpwlemdvds  12965  sqrt2irrap  12976  divdenle  12993  nonsq  13003  pythagtriplem4  13067  pclem0  13085  pcpremul  13092  pczdvds  13113  pcprmpw2  13132  qexpz  13151  4sqlem10  13186  ballotfilemimin  13298  ballotfilemsel1i  13305  ballotfilemro  13315  ennnfonelemkh  13352  triv1nsgd  14070  qusgrp  14084  gzsumsplit0  14197  prdsbaslemss  14223  bl2in  15553  xblcntrps  15563  xblcntr  15564  ssblps  15575  ssbl  15576  blssps  15577  blss  15578  xmetxp  15657  mulc1cncf  15739  cncfmptc  15746  mulcncflem  15757  ivthinclemlopn  15786  ivthinclemuopn  15788  ivthdec  15794  ivthreinc  15795  hovera  15797  hoverlt1  15799  limcimolemlt  15814  cnplimclemle  15818  cnplimclemr  15819  limccnp2lem  15826  dveflem  15876  reeff1olem  15921  reeff1oleme  15922  tangtx  15989  cosq34lt1  16001  logdivlti  16033  cxpap0  16059  rpabscxpbnd  16095  birthdaylem3  16146  pellexlem2  16149  ppiqp1le  16173  ppiqltx  16183  ppiqub  16194  mersenne  16195  bcmono  16202  bcmax  16203  bposlem2  16210  bposlem5  16213  lgslem3  16219  gausslemma2dlem1a  16275  lgsquadlem1  16294  lgsquadlem2  16295  2lgslem1c  16307  subumgredg2en  16610  qdencn  17170  cvgcmp2nlemabs  17179  trilpolemclim  17183  trilpolemisumle  17185  trilpolemeq1  17187  apdifflemf  17193  apdifflemr  17194