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  mulle0r  9274  lbinfle  9280  divge1  10124  ltesubnnd  10170  xltnegi  10237  xleadd1a  10275  xltadd1  10278  xlt2add  10282  xposdif  10284  xleaddadd  10289  lincmble  10406  ubmelm1fzo  10644  infssfzledc  10670  zsupssdc  10673  qbtwnrelemcalc  10690  qbtwnxr  10692  ceiqm1l  10748  ceilqm1lt  10749  ceilqle  10751  modqlt  10770  modqeqmodmin  10831  addmodlteq  10835  seqf1oglem1  10956  exp3vallem  10977  bernneq  11098  nn0ltexp2  11147  faclbnd2  11180  sshashneg  11281  ccatsymb  11370  ccatrn  11377  sq01  11660  resqrexlemdec  11777  resqrexlemcalc2  11781  resqrexlemglsq  11788  resqrexlemga  11789  abslt  11854  amgm2  11884  icodiamlt  11946  maxabsle  11970  maxltsup  11984  minmax  11996  min1inf  11998  min2inf  11999  bdtrilem  12005  xrmaxltsup  12024  xrmaxaddlem  12026  xrmaxadd  12027  xrminmax  12031  xrmin1inf  12033  xrmin2inf  12034  climconst  12056  serclim0  12071  mulcn2  12078  reccn2ap  12079  iserex  12105  climlec2  12107  iserge0  12109  climcau  12113  climcvg1nlem  12115  fsumabs  12232  iserabs  12242  isumlessdc  12263  divcnv  12264  expcnvre  12270  absgtap  12277  georeclim  12280  cvgratnnlembern  12290  cvgratnnlemsumlt  12295  cvgratnnlemfm  12296  cvgratnnlemrate  12297  mertenslemub  12301  mertenslemi1  12302  prodfclim1  12311  prodfap0  12312  efcvgfsum  12434  eftlub  12457  eflegeo  12468  tanval3ap  12481  tannegap  12495  ef01bndlem  12523  sin01bnd  12524  cos01bnd  12525  cos01gt0  12530  bitsfzolem  12721  bitsfzo  12722  bitsinv1lem  12728  mulgcd  12793  nnminle  12812  eucalglt  12835  lcmledvds  12848  mulgcddvds  12872  prmind2  12898  isprm5lem  12919  pw2dvdslemn  12943  pw2dvdseulemle  12945  oddpwdclemdvds  12948  sqrt2irrap  12958  divdenle  12975  nonsq  12985  pythagtriplem4  13047  pclem0  13065  pcpremul  13072  pczdvds  13093  pcprmpw2  13112  qexpz  13131  4sqlem10  13166  ballotfilemimin  13249  ballotfilemsel1i  13256  ballotfilemro  13266  ennnfonelemkh  13303  triv1nsgd  14021  qusgrp  14035  gzsumsplit0  14148  prdsbaslemss  14174  bl2in  15504  xblcntrps  15514  xblcntr  15515  ssblps  15526  ssbl  15527  blssps  15528  blss  15529  xmetxp  15608  mulc1cncf  15690  cncfmptc  15697  mulcncflem  15708  ivthinclemlopn  15737  ivthinclemuopn  15739  ivthdec  15745  ivthreinc  15746  hovera  15748  hoverlt1  15750  limcimolemlt  15765  cnplimclemle  15769  cnplimclemr  15770  limccnp2lem  15777  dveflem  15827  reeff1olem  15872  reeff1oleme  15873  tangtx  15939  cosq34lt1  15951  logdivlti  15982  cxpap0  16006  rpabscxpbnd  16042  birthdaylem3  16089  pellexlem2  16092  mersenne  16111  lgslem3  16121  gausslemma2dlem1a  16177  lgsquadlem1  16196  lgsquadlem2  16197  2lgslem1c  16209  subumgredg2en  16512  qdencn  17072  cvgcmp2nlemabs  17081  trilpolemclim  17085  trilpolemisumle  17087  trilpolemeq1  17089  apdifflemf  17095  apdifflemr  17096