Theorem eqbrtrd 4027

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

Syntax hints:   -> wi 4   = wceq 1353   class class class wbr 4005

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2741  df-un 3135  df-sn 3600  df-pr 3601  df-op 3603  df-br 4006

This theorem is referenced by:  eqbrtrrd  4029  dif1en  6881  ccfunen  7265  prarloclemcalc  7503  ltexprlemopu  7604  recexprlemloc  7632  caucvgprprlemloccalc  7685  suplocsrlem  7809  axpre-suploclemres  7902  mulle0r  8903  lbinfle  8909  divge1  9725  xltnegi  9837  xleadd1a  9875  xltadd1  9878  xlt2add  9882  xposdif  9884  xleaddadd  9889  ubmelm1fzo  10228  qbtwnrelemcalc  10258  qbtwnxr  10260  ceiqm1l  10313  ceilqm1lt  10314  ceilqle  10316  modqlt  10335  modqeqmodmin  10396  addmodlteq  10400  exp3vallem  10523  bernneq  10643  nn0ltexp2  10691  faclbnd2  10724  resqrexlemdec  11022  resqrexlemcalc2  11026  resqrexlemglsq  11033  resqrexlemga  11034  abslt  11099  amgm2  11129  icodiamlt  11191  maxabsle  11215  maxltsup  11229  minmax  11240  min1inf  11242  min2inf  11243  bdtrilem  11249  xrmaxltsup  11268  xrmaxaddlem  11270  xrmaxadd  11271  xrminmax  11275  xrmin1inf  11277  xrmin2inf  11278  climconst  11300  serclim0  11315  mulcn2  11322  reccn2ap  11323  iserex  11349  climlec2  11351  iserge0  11353  climcau  11357  climcvg1nlem  11359  fsumabs  11475  iserabs  11485  isumlessdc  11506  divcnv  11507  expcnvre  11513  absgtap  11520  georeclim  11523  cvgratnnlembern  11533  cvgratnnlemsumlt  11538  cvgratnnlemfm  11539  cvgratnnlemrate  11540  mertenslemub  11544  mertenslemi1  11545  prodfclim1  11554  prodfap0  11555  efcvgfsum  11677  eftlub  11700  eflegeo  11711  tanval3ap  11724  tannegap  11738  ef01bndlem  11766  sin01bnd  11767  cos01bnd  11768  cos01gt0  11772  zsupssdc  11957  mulgcd  12019  nnminle  12038  eucalglt  12059  lcmledvds  12072  mulgcddvds  12096  prmind2  12122  isprm5lem  12143  pw2dvdslemn  12167  pw2dvdseulemle  12169  oddpwdclemdvds  12172  sqrt2irrap  12182  divdenle  12199  nonsq  12209  pythagtriplem4  12270  pclem0  12288  pcpremul  12295  pczdvds  12315  pcprmpw2  12334  qexpz  12352  4sqlem10  12387  ennnfonelemkh  12415  triv1nsgd  13083  bl2in  13988  xblcntrps  13998  xblcntr  13999  ssblps  14010  ssbl  14011  blssps  14012  blss  14013  xmetxp  14092  mulc1cncf  14161  cncfmptc  14167  mulcncflem  14175  ivthinclemlopn  14199  ivthinclemuopn  14201  ivthdec  14207  limcimolemlt  14218  cnplimclemle  14222  cnplimclemr  14223  limccnp2lem  14230  dveflem  14272  reeff1olem  14277  reeff1oleme  14278  tangtx  14344  cosq34lt1  14356  logdivlti  14387  cxpap0  14410  rpabscxpbnd  14444  lgslem3  14488  qdencn  14860  cvgcmp2nlemabs  14865  trilpolemclim  14869  trilpolemisumle  14871  trilpolemeq1  14873  apdifflemf  14879  apdifflemr  14880