Theorem breqtrd 3962

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)

Hypotheses

Ref	Expression
breqtrd.1	|- ( ph -> A R B )
breqtrd.2	|- ( ph -> B = C )

Assertion

Ref	Expression
breqtrd	|- ( ph -> A R C )

Proof of Theorem breqtrd

Step	Hyp	Ref	Expression
1		breqtrd.1	. 2 |- ( ph -> A R B )
2		breqtrd.2	. . 3 |- ( ph -> B = C )
3	2	breq2d 3949	. 2 |- ( ph -> ( A R B <-> A R C ) )
4	1, 3	mpbid 146	1 |- ( ph -> A R C )

Syntax hints:   -> wi 4   = wceq 1332   class class class wbr 3937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-un 3080  df-sn 3538  df-pr 3539  df-op 3541  df-br 3938

This theorem is referenced by:  breqtrrd  3964  breqtrid  3973  tfrexlem  6239  phplem4  6757  phplem4on  6769  fidifsnen  6772  fisbth  6785  fin0  6787  fin0or  6788  ltsonq  7230  addlocprlemeqgt  7364  prmuloclemcalc  7397  mullocprlem  7402  addcanprlemu  7447  ltaprlem  7450  ltaprg  7451  prplnqu  7452  ltmprr  7474  cauappcvgprlemopl  7478  cauappcvgprlemloc  7484  cauappcvgprlemladdru  7488  cauappcvgprlemladdrl  7489  cauappcvgprlem1  7491  caucvgprlemm  7500  caucvgprlemopl  7501  caucvgprlemloc  7507  caucvgprprlemloccalc  7516  caucvgprprlemopl  7529  recexgt0sr  7605  ltm1sr  7609  prsrpos  7617  caucvgsrlemoffgt1  7631  caucvgsr  7634  suplocsrlempr  7639  pitoregt0  7681  axpre-suploclemres  7733  add20  8260  mullt0  8266  ltmul1a  8377  ltm1  8628  recgt0  8632  prodgt0gt0  8633  prodgt0  8634  prodge0  8636  lemul1a  8640  recp1lt1  8681  recreclt  8682  ledivp1  8685  mulle0r  8726  ltaddrp2d  9548  mul2lt0np  9580  xleadd1a  9686  xleaddadd  9700  fz01en  9864  fzonmapblen  9995  qbtwnrelemcalc  10064  flqaddz  10101  flhalf  10106  flqdiv  10125  modqmuladdim  10171  modqsubdir  10197  addmodlteq  10202  frecfzen2  10231  iseqf1olemab  10293  ser3le  10322  ltexp2a  10376  leexp2a  10377  exple1  10380  expubnd  10381  bernneq  10443  faclbnd6  10522  hashfz  10599  zfz1isolemiso  10614  zfz1iso  10616  seq3coll  10617  cvg1nlemcxze  10786  cvg1nlemres  10789  recvguniqlem  10798  resqrexlemover  10814  resqrexlemdec  10815  resqrexlemcalc2  10819  resqrexlemcalc3  10820  resqrexlemnm  10822  resqrexlemoverl  10825  ltabs  10891  abslt  10892  absle  10893  abstri  10908  maxabslemlub  11011  maxabslemval  11012  dfabsmax  11021  bdtrilem  11042  xrmaxiflemab  11048  xrmaxiflemlub  11049  xrmaxaddlem  11061  reccn2ap  11114  climge0  11126  climaddc2  11131  summodclem2a  11182  zsumdc  11185  isumge0  11231  fsumle  11264  fsumlt  11265  isumshft  11291  expcnvap0  11303  geolim  11312  geolim2  11313  georeclim  11314  geo2lim  11317  cvgratnnlembern  11324  cvgratnnlemfm  11330  mertenslemi1  11336  mertensabs  11338  prodmodclem3  11376  prodmodclem2a  11377  zproddc  11380  fprodseq  11384  efcllemp  11401  ef0lem  11403  efgt0  11427  eftlub  11433  efltim  11441  sinbnd  11495  cosbnd  11496  ef01bndlem  11499  sin01gt0  11504  cos01gt0  11505  sin02gt0  11506  eirraplem  11519  dvdssub2  11571  dvdsadd2b  11576  dvdsexp  11595  opoe  11628  divalglemeunn  11654  divalglemex  11655  divalglemeuneg  11656  gcdaddm  11708  bezoutlemstep  11721  dvdsgcd  11736  dvdsmulgcd  11749  bezoutr1  11757  nn0seqcvgd  11758  rpmulgcd2  11812  qredeq  11813  rpdvds  11816  prmind2  11837  divdenle  11911  phicl2  11926  hashdvds  11933  phimullem  11937  ennnfonelemkh  11961  ennnfonelemnn0  11971  psmetsym  12537  psmettri  12538  mettri2  12570  xmetsym  12576  xmettri  12580  metrtri  12585  xblss2ps  12612  xblss2  12613  blhalf  12616  xmsge0  12675  cnmet  12738  ivthinclemlopn  12822  dveflem  12895  dvef  12896  sin0pilem1  12910  sinq12gt0  12959  sinq34lt0t  12960  cosq14gt0  12961  coseq0q4123  12963  rpabscxpbnd  13067  logbgcd1irraplemexp  13093  pwf1oexmid  13367  qdencn  13397  cvgcmp2nlemabs  13402  apdifflemf  13414  apdifflemr  13415