Theorem eqbrtrd 4051

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

Syntax hints:   -> wi 4   = wceq 1364   class class class wbr 4029

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3157  df-sn 3624  df-pr 3625  df-op 3627  df-br 4030

This theorem is referenced by:  eqbrtrrd  4053  dif1en  6935  ccfunen  7324  prarloclemcalc  7562  ltexprlemopu  7663  recexprlemloc  7691  caucvgprprlemloccalc  7744  suplocsrlem  7868  axpre-suploclemres  7961  mulle0r  8963  lbinfle  8969  divge1  9789  xltnegi  9901  xleadd1a  9939  xltadd1  9942  xlt2add  9946  xposdif  9948  xleaddadd  9953  ubmelm1fzo  10293  qbtwnrelemcalc  10324  qbtwnxr  10326  ceiqm1l  10382  ceilqm1lt  10383  ceilqle  10385  modqlt  10404  modqeqmodmin  10465  addmodlteq  10469  seqf1oglem1  10590  exp3vallem  10611  bernneq  10731  nn0ltexp2  10780  faclbnd2  10813  resqrexlemdec  11155  resqrexlemcalc2  11159  resqrexlemglsq  11166  resqrexlemga  11167  abslt  11232  amgm2  11262  icodiamlt  11324  maxabsle  11348  maxltsup  11362  minmax  11373  min1inf  11375  min2inf  11376  bdtrilem  11382  xrmaxltsup  11401  xrmaxaddlem  11403  xrmaxadd  11404  xrminmax  11408  xrmin1inf  11410  xrmin2inf  11411  climconst  11433  serclim0  11448  mulcn2  11455  reccn2ap  11456  iserex  11482  climlec2  11484  iserge0  11486  climcau  11490  climcvg1nlem  11492  fsumabs  11608  iserabs  11618  isumlessdc  11639  divcnv  11640  expcnvre  11646  absgtap  11653  georeclim  11656  cvgratnnlembern  11666  cvgratnnlemsumlt  11671  cvgratnnlemfm  11672  cvgratnnlemrate  11673  mertenslemub  11677  mertenslemi1  11678  prodfclim1  11687  prodfap0  11688  efcvgfsum  11810  eftlub  11833  eflegeo  11844  tanval3ap  11857  tannegap  11871  ef01bndlem  11899  sin01bnd  11900  cos01bnd  11901  cos01gt0  11906  zsupssdc  12091  mulgcd  12153  nnminle  12172  eucalglt  12195  lcmledvds  12208  mulgcddvds  12232  prmind2  12258  isprm5lem  12279  pw2dvdslemn  12303  pw2dvdseulemle  12305  oddpwdclemdvds  12308  sqrt2irrap  12318  divdenle  12335  nonsq  12345  pythagtriplem4  12406  pclem0  12424  pcpremul  12431  pczdvds  12452  pcprmpw2  12471  qexpz  12490  4sqlem10  12525  ennnfonelemkh  12569  triv1nsgd  13288  qusgrp  13302  bl2in  14571  xblcntrps  14581  xblcntr  14582  ssblps  14593  ssbl  14594  blssps  14595  blss  14596  xmetxp  14675  mulc1cncf  14744  cncfmptc  14750  mulcncflem  14761  ivthinclemlopn  14790  ivthinclemuopn  14792  ivthdec  14798  ivthreinc  14799  hovera  14801  hoverlt1  14803  limcimolemlt  14818  cnplimclemle  14822  cnplimclemr  14823  limccnp2lem  14830  dveflem  14872  reeff1olem  14906  reeff1oleme  14907  tangtx  14973  cosq34lt1  14985  logdivlti  15016  cxpap0  15039  rpabscxpbnd  15073  lgslem3  15118  gausslemma2dlem1a  15174  lgsquadlem1  15191  qdencn  15517  cvgcmp2nlemabs  15522  trilpolemclim  15526  trilpolemisumle  15528  trilpolemeq1  15530  apdifflemf  15536  apdifflemr  15537