Theorem breqtrd 4140

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 4126	. 2 |- ( ph -> ( A R B <-> A R C ) )
4	1, 3	mpbid 147	1 |- ( ph -> A R C )

Syntax hints:   -> wi 4   = wceq 1398   class class class wbr 4114

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703  df-br 4115

This theorem is referenced by:  breqtrrd  4142  breqtrid  4151  tfrexlem  6578  phplem4  7122  phplem4on  7135  fidifsnen  7138  fisbth  7153  fin0  7155  fin0or  7156  ltsonq  7729  addlocprlemeqgt  7863  prmuloclemcalc  7896  mullocprlem  7901  addcanprlemu  7946  ltaprlem  7949  ltaprg  7950  prplnqu  7951  ltmprr  7973  cauappcvgprlemopl  7977  cauappcvgprlemloc  7983  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  cauappcvgprlem1  7990  caucvgprlemm  7999  caucvgprlemopl  8000  caucvgprlemloc  8006  caucvgprprlemloccalc  8015  caucvgprprlemopl  8028  recexgt0sr  8104  ltm1sr  8108  prsrpos  8116  caucvgsrlemoffgt1  8130  caucvgsr  8133  suplocsrlempr  8138  pitoregt0  8180  axpre-suploclemres  8232  add20  8766  mullt0  8772  ltmul1a  8883  ltm1  9140  recgt0  9144  prodgt0gt0  9145  prodgt0  9146  prodge0  9148  lemul1a  9152  recp1lt1  9193  recreclt  9194  ledivp1  9197  mulle0r  9238  eluzmn  9881  ltaddrp2d  10085  mul2lt0np  10117  xleadd1a  10228  xleaddadd  10242  lincmble  10359  fz01en  10411  fzonmapblen  10551  qbtwnrelemcalc  10642  flqaddz  10684  flhalf  10689  flqdiv  10710  modqmuladdim  10756  modqsubdir  10782  addmodlteq  10787  frecfzen2  10816  iseqf1olemab  10891  ser3le  10926  ltexp2a  10980  leexp2a  10981  exple1  10984  expubnd  10985  bernneq  11050  faclbnd6  11134  hashfz  11214  zfz1isolemiso  11239  zfz1iso  11241  seq3coll  11242  cvg1nlemcxze  11695  cvg1nlemres  11698  recvguniqlem  11707  resqrexlemover  11723  resqrexlemdec  11724  resqrexlemcalc2  11728  resqrexlemcalc3  11729  resqrexlemnm  11731  resqrexlemoverl  11734  ltabs  11800  abslt  11801  absle  11802  abstri  11817  maxabslemlub  11920  maxabslemval  11921  dfabsmax  11930  bdtrilem  11952  xrmaxiflemab  11960  xrmaxiflemlub  11961  xrmaxaddlem  11973  reccn2ap  12026  climge0  12038  climaddc2  12043  summodclem2a  12095  zsumdc  12098  isumge0  12144  fsumle  12177  fsumlt  12178  isumshft  12204  expcnvap0  12216  geolim  12225  geolim2  12226  georeclim  12227  geo2lim  12230  cvgratnnlembern  12237  cvgratnnlemfm  12243  mertenslemi1  12249  mertensabs  12251  prodmodclem3  12289  prodmodclem2a  12290  zproddc  12293  fprodseq  12297  efcllemp  12372  ef0lem  12374  efgt0  12398  eftlub  12404  efltim  12412  sinbnd  12466  cosbnd  12467  ef01bndlem  12470  sin01gt0  12476  cos01gt0  12477  sin02gt0  12478  eirraplem  12491  dvdssub2  12549  dvdsadd2b  12554  dvdsexp  12575  3dvds  12578  opoe  12609  divalglemeunn  12635  divalglemex  12636  divalglemeuneg  12637  bitsfzolem  12668  bitsinv1lem  12675  gcdaddm  12708  bezoutlemstep  12721  dvdsgcd  12736  dvdsmulgcd  12749  bezoutr1  12757  nninfctlemfo  12764  nn0seqcvgd  12766  rpmulgcd2  12820  qredeq  12821  rpdvds  12824  prmind2  12845  divdenle  12922  phicl2  12939  hashdvds  12946  phimullem  12950  eulerthlemth  12957  prmdiveq  12961  prmdivdiv  12962  pythagtriplem4  12994  pythagtriplem10  12995  pythagtriplem19  13008  pcpre1  13018  pcadd2  13067  qexpz  13078  expnprm  13079  oddprmdvds  13080  pockthlem  13082  4sqlem7  13110  4sqlem10  13113  4sqexercise1  13124  4sqexercise2  13125  4sqlemsdc  13126  4sqlem11  13127  4sqlem12  13128  4sqlem14  13130  4sqlem15  13131  4sqlem16  13132  ennnfonelemkh  13250  ennnfonelemnn0  13260  qusgrp  13988  dvdsrid  14348  dvdsrtr  14349  dvdsrneg  14351  unitmulcl  14361  unitgrp  14364  unitnegcl  14378  subrguss  14485  subrgunit  14488  znidomb  14935  psmetsym  15323  psmettri  15324  mettri2  15356  xmetsym  15362  xmettri  15366  metrtri  15371  xblss2ps  15398  xblss2  15399  blhalf  15402  xmsge0  15461  cnmet  15524  ivthinclemlopn  15630  ivthdichlem  15645  dveflem  15720  dvef  15721  plyaddlem1  15741  sin0pilem1  15775  sinq12gt0  15824  sinq34lt0t  15825  cosq14gt0  15826  coseq0q4123  15828  rpabscxpbnd  15934  logbgcd1irraplemexp  15962  dvdsppwf1o  15986  mpodvdsmulf1o  15987  perfectlem2  15997  lgslem1  16002  lgseisenlem2  16073  lgsquadlem1  16079  lgsquadlem2  16080  lgsquad2lem1  16083  2sqlem3  16119  2sqlem4  16120  2sqlem8  16125  dichmul0orlem1  16636  pwf1oexmid  16912  qdencn  16946  cvgcmp2nlemabs  16955  apdifflemf  16969  apdifflemr  16970