Theorem breqtrd 4137

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 4123	. 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 4111

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 3217  df-sn 3697  df-pr 3698  df-op 3700  df-br 4112

This theorem is referenced by:  breqtrrd  4139  breqtrid  4148  tfrexlem  6567  phplem4  7111  phplem4on  7124  fidifsnen  7127  fisbth  7142  fin0  7144  fin0or  7145  ltsonq  7715  addlocprlemeqgt  7849  prmuloclemcalc  7882  mullocprlem  7887  addcanprlemu  7932  ltaprlem  7935  ltaprg  7936  prplnqu  7937  ltmprr  7959  cauappcvgprlemopl  7963  cauappcvgprlemloc  7969  cauappcvgprlemladdru  7973  cauappcvgprlemladdrl  7974  cauappcvgprlem1  7976  caucvgprlemm  7985  caucvgprlemopl  7986  caucvgprlemloc  7992  caucvgprprlemloccalc  8001  caucvgprprlemopl  8014  recexgt0sr  8090  ltm1sr  8094  prsrpos  8102  caucvgsrlemoffgt1  8116  caucvgsr  8119  suplocsrlempr  8124  pitoregt0  8166  axpre-suploclemres  8218  add20  8750  mullt0  8756  ltmul1a  8867  ltm1  9122  recgt0  9126  prodgt0gt0  9127  prodgt0  9128  prodge0  9130  lemul1a  9134  recp1lt1  9175  recreclt  9176  ledivp1  9179  mulle0r  9220  eluzmn  9863  ltaddrp2d  10067  mul2lt0np  10099  xleadd1a  10209  xleaddadd  10223  lincmble  10340  fz01en  10390  fzonmapblen  10530  qbtwnrelemcalc  10619  flqaddz  10661  flhalf  10666  flqdiv  10687  modqmuladdim  10733  modqsubdir  10759  addmodlteq  10764  frecfzen2  10793  iseqf1olemab  10868  ser3le  10903  ltexp2a  10957  leexp2a  10958  exple1  10961  expubnd  10962  bernneq  11026  faclbnd6  11110  hashfz  11190  zfz1isolemiso  11215  zfz1iso  11217  seq3coll  11218  cvg1nlemcxze  11671  cvg1nlemres  11674  recvguniqlem  11683  resqrexlemover  11699  resqrexlemdec  11700  resqrexlemcalc2  11704  resqrexlemcalc3  11705  resqrexlemnm  11707  resqrexlemoverl  11710  ltabs  11776  abslt  11777  absle  11778  abstri  11793  maxabslemlub  11896  maxabslemval  11897  dfabsmax  11906  bdtrilem  11928  xrmaxiflemab  11936  xrmaxiflemlub  11937  xrmaxaddlem  11949  reccn2ap  12002  climge0  12014  climaddc2  12019  summodclem2a  12071  zsumdc  12074  isumge0  12120  fsumle  12153  fsumlt  12154  isumshft  12180  expcnvap0  12192  geolim  12201  geolim2  12202  georeclim  12203  geo2lim  12206  cvgratnnlembern  12213  cvgratnnlemfm  12219  mertenslemi1  12225  mertensabs  12227  prodmodclem3  12265  prodmodclem2a  12266  zproddc  12269  fprodseq  12273  efcllemp  12348  ef0lem  12350  efgt0  12374  eftlub  12380  efltim  12388  sinbnd  12442  cosbnd  12443  ef01bndlem  12446  sin01gt0  12452  cos01gt0  12453  sin02gt0  12454  eirraplem  12467  dvdssub2  12525  dvdsadd2b  12530  dvdsexp  12551  3dvds  12554  opoe  12585  divalglemeunn  12611  divalglemex  12612  divalglemeuneg  12613  bitsfzolem  12644  bitsinv1lem  12651  gcdaddm  12684  bezoutlemstep  12697  dvdsgcd  12712  dvdsmulgcd  12725  bezoutr1  12733  nninfctlemfo  12740  nn0seqcvgd  12742  rpmulgcd2  12796  qredeq  12797  rpdvds  12800  prmind2  12821  divdenle  12898  phicl2  12915  hashdvds  12922  phimullem  12926  eulerthlemth  12933  prmdiveq  12937  prmdivdiv  12938  pythagtriplem4  12970  pythagtriplem10  12971  pythagtriplem19  12984  pcpre1  12994  pcadd2  13043  qexpz  13054  expnprm  13055  oddprmdvds  13056  pockthlem  13058  4sqlem7  13086  4sqlem10  13089  4sqexercise1  13100  4sqexercise2  13101  4sqlemsdc  13102  4sqlem11  13103  4sqlem12  13104  4sqlem14  13106  4sqlem15  13107  4sqlem16  13108  ennnfonelemkh  13180  ennnfonelemnn0  13190  qusgrp  13966  dvdsrid  14262  dvdsrtr  14263  dvdsrneg  14265  unitmulcl  14275  unitgrp  14278  unitnegcl  14292  subrguss  14398  subrgunit  14401  znidomb  14823  psmetsym  15211  psmettri  15212  mettri2  15244  xmetsym  15250  xmettri  15254  metrtri  15259  xblss2ps  15286  xblss2  15287  blhalf  15290  xmsge0  15349  cnmet  15412  ivthinclemlopn  15518  ivthdichlem  15533  dveflem  15608  dvef  15609  plyaddlem1  15629  sin0pilem1  15663  sinq12gt0  15712  sinq34lt0t  15713  cosq14gt0  15714  coseq0q4123  15716  rpabscxpbnd  15822  logbgcd1irraplemexp  15850  dvdsppwf1o  15874  mpodvdsmulf1o  15875  perfectlem2  15885  lgslem1  15890  lgseisenlem2  15961  lgsquadlem1  15967  lgsquadlem2  15968  lgsquad2lem1  15971  2sqlem3  16007  2sqlem4  16008  2sqlem8  16013  pwf1oexmid  16790  qdencn  16824  cvgcmp2nlemabs  16833  apdifflemf  16847  apdifflemr  16848