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  6609  phplem4  7160  phplem4on  7173  fidifsnen  7176  fisbth  7191  fin0  7193  fin0or  7194  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  9944  irraddap  10063  ltaddrp2d  10149  mul2lt0np  10181  xleadd1a  10292  xleaddadd  10306  lincmble  10423  fz01en  10476  fzonmapblen  10616  qbtwnrelemcalc  10707  flqaddz  10753  flhalf  10758  flqdiv  10779  modqmuladdim  10825  modqsubdir  10851  addmodlteq  10856  frecfzen2  10885  iseqf1olemab  10960  ser3le  10995  ltexp2a  11049  leexp2a  11050  exple1  11053  expubnd  11054  bernneq  11119  faclbnd6  11204  hashfz  11284  zfz1isolemiso  11313  zfz1iso  11315  seq3coll  11316  cvg1nlemcxze  11770  cvg1nlemres  11773  recvguniqlem  11782  resqrexlemover  11798  resqrexlemdec  11799  resqrexlemcalc2  11803  resqrexlemcalc3  11804  resqrexlemnm  11806  resqrexlemoverl  11809  ltabs  11876  abslt  11877  absle  11878  abstri  11893  maxabslemlub  11996  maxabslemval  11997  dfabsmax  12006  bdtrilem  12030  xrmaxiflemab  12038  xrmaxiflemlub  12039  xrmaxaddlem  12051  reccn2ap  12104  climge0  12116  climaddc2  12121  summodclem2a  12173  zsumdc  12176  isumge0  12222  fsumle  12255  fsumlt  12256  isumshft  12282  expcnvap0  12294  geolim  12303  geolim2  12304  georeclim  12305  geo2lim  12308  cvgratnnlembern  12315  cvgratnnlemfm  12321  mertenslemi1  12327  mertensabs  12329  prodmodclem3  12367  prodmodclem2a  12368  zproddc  12371  fprodseq  12375  efcllemp  12450  ef0lem  12452  efgt0  12476  eftlub  12482  efltim  12490  sinbnd  12544  cosbnd  12545  ef01bndlem  12548  sin01gt0  12554  cos01gt0  12555  sin02gt0  12556  eirraplem  12569  dvdssub2  12627  dvdsadd2b  12632  dvdsexp  12653  3dvds  12656  opoe  12687  divalglemeunn  12713  divalglemex  12714  divalglemeuneg  12715  bitsfzolem  12746  bitsinv1lem  12753  gcdaddm  12786  bezoutlemstep  12799  dvdsgcd  12814  dvdsmulgcd  12827  bezoutr1  12835  nninfctlemfo  12842  nn0seqcvgd  12844  rpmulgcd2  12898  qredeq  12899  rpdvds  12902  prmind2  12923  divdenle  13002  phicl2  13021  hashdvds  13028  phimullem  13032  eulerthlemth  13039  prmdiveq  13043  prmdivdiv  13044  pythagtriplem4  13076  pythagtriplem10  13077  pythagtriplem19  13090  pcpre1  13100  pcadd2  13149  qexpz  13160  expnprm  13161  oddprmdvds  13162  pockthlem  13164  4sqlem7  13192  4sqlem10  13195  4sqexercise1  13206  4sqexercise2  13207  4sqlemsdc  13208  4sqlem11  13209  4sqlem12  13210  4sqlem14  13212  4sqlem15  13213  4sqlem16  13214  ennnfonelemkh  13361  ennnfonelemnn0  13371  qusgrp  14094  dvdsrid  14516  dvdsrtr  14517  dvdsrneg  14519  unitmulcl  14529  unitgrp  14532  unitnegcl  14546  subrguss  14653  subrgunit  14656  znidomb  15102  psmetsym  15555  psmettri  15556  mettri2  15588  xmetsym  15594  xmettri  15598  metrtri  15603  xblss2ps  15630  xblss2  15631  blhalf  15634  xmsge0  15693  cnmet  15756  ivthinclemlopn  15862  ivthdichlem  15877  dveflem  15952  dvef  15953  plyaddlem1  15973  sin0pilem1  16008  sinq12gt0  16057  sinq34lt0t  16058  cosq14gt0  16059  coseq0q4123  16061  logdivlt  16124  rpabscxpbnd  16175  logbgcd1irraplemexp  16204  log2tlbndlog2  16220  birthdaylem2  16226  birthdaylem3  16227  dvdsppwf1o  16283  mpodvdsmulf1o  16284  chtqub  16296  perfectlem2  16300  bclbnd  16307  bposlem1  16311  bposlem3  16313  bposlem4  16314  bposlem6  16316  lgslem1  16324  lgseisenlem2  16395  lgsquadlem1  16401  lgsquadlem2  16402  lgsquad2lem1  16405  2sqlem3  16441  2sqlem4  16442  2sqlem8  16447  dichmul0orlem1  16958  pwf1oexmid  17234  qdencn  17278  cvgcmp2nlemabs  17287  apdifflemf  17302  apdifflemr  17303