Theorem breqtrd 4157

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   class class class wbr 4131

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-br 4132

This theorem is used by:  breqtrrd  4159  breqtrid  4168  tfrexlem  6610  phplem4  7162  phplem4on  7175  fidifsnen  7178  fisbth  7193  fin0  7195  fin0or  7196  ltsonq  7771  addlocprlemeqgt  7905  prmuloclemcalc  7938  mullocprlem  7943  addcanprlemu  7988  ltaprlem  7991  ltaprg  7992  prplnqu  7993  ltmprr  8015  cauappcvgprlemopl  8019  cauappcvgprlemloc  8025  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  cauappcvgprlem1  8032  caucvgprlemm  8041  caucvgprlemopl  8042  caucvgprlemloc  8048  caucvgprprlemloccalc  8057  caucvgprprlemopl  8070  recexgt0sr  8146  ltm1sr  8150  prsrpos  8158  caucvgsrlemoffgt1  8172  caucvgsr  8175  suplocsrlempr  8180  pitoregt0  8222  axpre-suploclemres  8274  add20  8809  mullt0  8815  ltmul1a  8927  ltm1  9184  recgt0  9188  prodgt0gt0  9189  prodgt0  9190  prodge0  9192  lemul1a  9196  recp1lt1  9237  recreclt  9238  ledivp1  9241  mulle0r  9282  eluzmn  9943  irraddap  10062  ltaddrp2d  10148  mul2lt0np  10180  xleadd1a  10291  xleaddadd  10305  lincmble  10422  fz01en  10475  fzonmapblen  10615  qbtwnrelemcalc  10706  flqaddz  10752  flhalf  10757  flqdiv  10778  modqmuladdim  10824  modqsubdir  10850  addmodlteq  10855  frecfzen2  10884  iseqf1olemab  10959  ser3le  10994  ltexp2a  11048  leexp2a  11049  exple1  11052  expubnd  11053  bernneq  11118  faclbnd6  11203  hashfz  11283  zfz1isolemiso  11312  zfz1iso  11314  seq3coll  11315  cvg1nlemcxze  11769  cvg1nlemres  11772  recvguniqlem  11781  resqrexlemover  11797  resqrexlemdec  11798  resqrexlemcalc2  11802  resqrexlemcalc3  11803  resqrexlemnm  11805  resqrexlemoverl  11808  ltabs  11875  abslt  11876  absle  11877  abstri  11892  maxabslemlub  11995  maxabslemval  11996  dfabsmax  12005  bdtrilem  12029  xrmaxiflemab  12037  xrmaxiflemlub  12038  xrmaxaddlem  12050  reccn2ap  12103  climge0  12115  climaddc2  12120  summodclem2a  12172  zsumdc  12175  isumge0  12221  fsumle  12254  fsumlt  12255  isumshft  12281  expcnvap0  12293  geolim  12302  geolim2  12303  georeclim  12304  geo2lim  12307  cvgratnnlembern  12314  cvgratnnlemfm  12320  mertenslemi1  12326  mertensabs  12328  prodmodclem3  12366  prodmodclem2a  12367  zproddc  12370  fprodseq  12374  efcllemp  12449  ef0lem  12451  efgt0  12475  eftlub  12481  efltim  12489  sinbnd  12543  cosbnd  12544  ef01bndlem  12547  sin01gt0  12553  cos01gt0  12554  sin02gt0  12555  eirraplem  12568  dvdssub2  12626  dvdsadd2b  12631  dvdsexp  12652  3dvds  12655  opoe  12686  divalglemeunn  12712  divalglemex  12713  divalglemeuneg  12714  bitsfzolem  12745  bitsinv1lem  12752  gcdaddm  12785  bezoutlemstep  12798  dvdsgcd  12813  dvdsmulgcd  12826  bezoutr1  12834  nninfctlemfo  12841  nn0seqcvgd  12843  rpmulgcd2  12897  qredeq  12898  rpdvds  12901  prmind2  12922  divdenle  13001  phicl2  13020  hashdvds  13027  phimullem  13031  eulerthlemth  13038  prmdiveq  13042  prmdivdiv  13043  pythagtriplem4  13075  pythagtriplem10  13076  pythagtriplem19  13089  pcpre1  13099  pcadd2  13148  qexpz  13159  expnprm  13160  oddprmdvds  13161  pockthlem  13163  4sqlem7  13191  4sqlem10  13194  4sqexercise1  13205  4sqexercise2  13206  4sqlemsdc  13207  4sqlem11  13208  4sqlem12  13209  4sqlem14  13211  4sqlem15  13212  4sqlem16  13213  ennnfonelemkh  13360  ennnfonelemnn0  13370  qusgrp  14093  dvdsrid  14515  dvdsrtr  14516  dvdsrneg  14518  unitmulcl  14528  unitgrp  14531  unitnegcl  14545  subrguss  14652  subrgunit  14655  znidomb  15101  psmetsym  15572  psmettri  15573  mettri2  15605  xmetsym  15611  xmettri  15615  metrtri  15620  xblss2ps  15647  xblss2  15648  blhalf  15651  xmsge0  15710  cnmet  15773  ivthinclemlopn  15879  ivthdichlem  15894  dveflem  15969  dvef  15970  plyaddlem1  15990  sin0pilem1  16025  sinq12gt0  16074  sinq34lt0t  16075  cosq14gt0  16076  coseq0q4123  16078  logdivlt  16141  rpabscxpbnd  16192  logbgcd1irraplemexp  16221  log2tlbndlog2  16237  birthdaylem2  16243  birthdaylem3  16244  dvdsppwf1o  16300  mpodvdsmulf1o  16301  chtqub  16313  perfectlem2  16317  bclbnd  16324  bposlem1  16328  bposlem3  16330  bposlem4  16331  bposlem6  16333  lgslem1  16341  lgseisenlem2  16412  lgsquadlem1  16418  lgsquadlem2  16419  lgsquad2lem1  16422  2sqlem3  16458  2sqlem4  16459  2sqlem8  16464  dichmul0orlem1  16975  pwf1oexmid  17251  qdencn  17295  cvgcmp2nlemabs  17304  apdifflemf  17319  apdifflemr  17320