Theorem breqtrd 4154

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

Syntax hints:   -> wi 4   = wceq 1402   class class class wbr 4128

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 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 theorem 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 3714  df-pr 3715  df-op 3717  df-br 4129

This theorem is referenced by:  breqtrrd  4156  breqtrid  4165  tfrexlem  6598  phplem4  7149  phplem4on  7162  fidifsnen  7165  fisbth  7180  fin0  7182  fin0or  7183  ltsonq  7758  addlocprlemeqgt  7892  prmuloclemcalc  7925  mullocprlem  7930  addcanprlemu  7975  ltaprlem  7978  ltaprg  7979  prplnqu  7980  ltmprr  8002  cauappcvgprlemopl  8006  cauappcvgprlemloc  8012  cauappcvgprlemladdru  8016  cauappcvgprlemladdrl  8017  cauappcvgprlem1  8019  caucvgprlemm  8028  caucvgprlemopl  8029  caucvgprlemloc  8035  caucvgprprlemloccalc  8044  caucvgprprlemopl  8057  recexgt0sr  8133  ltm1sr  8137  prsrpos  8145  caucvgsrlemoffgt1  8159  caucvgsr  8162  suplocsrlempr  8167  pitoregt0  8209  axpre-suploclemres  8261  add20  8795  mullt0  8801  ltmul1a  8912  ltm1  9169  recgt0  9173  prodgt0gt0  9174  prodgt0  9175  prodge0  9177  lemul1a  9181  recp1lt1  9222  recreclt  9223  ledivp1  9226  mulle0r  9267  eluzmn  9910  ltaddrp2d  10114  mul2lt0np  10146  xleadd1a  10257  xleaddadd  10271  lincmble  10388  fz01en  10440  fzonmapblen  10580  qbtwnrelemcalc  10671  flqaddz  10713  flhalf  10718  flqdiv  10739  modqmuladdim  10785  modqsubdir  10811  addmodlteq  10816  frecfzen2  10845  iseqf1olemab  10920  ser3le  10955  ltexp2a  11009  leexp2a  11010  exple1  11013  expubnd  11014  bernneq  11079  faclbnd6  11163  hashfz  11243  zfz1isolemiso  11272  zfz1iso  11274  seq3coll  11275  cvg1nlemcxze  11729  cvg1nlemres  11732  recvguniqlem  11741  resqrexlemover  11757  resqrexlemdec  11758  resqrexlemcalc2  11762  resqrexlemcalc3  11763  resqrexlemnm  11765  resqrexlemoverl  11768  ltabs  11834  abslt  11835  absle  11836  abstri  11851  maxabslemlub  11954  maxabslemval  11955  dfabsmax  11964  bdtrilem  11986  xrmaxiflemab  11994  xrmaxiflemlub  11995  xrmaxaddlem  12007  reccn2ap  12060  climge0  12072  climaddc2  12077  summodclem2a  12129  zsumdc  12132  isumge0  12178  fsumle  12211  fsumlt  12212  isumshft  12238  expcnvap0  12250  geolim  12259  geolim2  12260  georeclim  12261  geo2lim  12264  cvgratnnlembern  12271  cvgratnnlemfm  12277  mertenslemi1  12283  mertensabs  12285  prodmodclem3  12323  prodmodclem2a  12324  zproddc  12327  fprodseq  12331  efcllemp  12406  ef0lem  12408  efgt0  12432  eftlub  12438  efltim  12446  sinbnd  12500  cosbnd  12501  ef01bndlem  12504  sin01gt0  12510  cos01gt0  12511  sin02gt0  12512  eirraplem  12525  dvdssub2  12583  dvdsadd2b  12588  dvdsexp  12609  3dvds  12612  opoe  12643  divalglemeunn  12669  divalglemex  12670  divalglemeuneg  12671  bitsfzolem  12702  bitsinv1lem  12709  gcdaddm  12742  bezoutlemstep  12755  dvdsgcd  12770  dvdsmulgcd  12783  bezoutr1  12791  nninfctlemfo  12798  nn0seqcvgd  12800  rpmulgcd2  12854  qredeq  12855  rpdvds  12858  prmind2  12879  divdenle  12956  phicl2  12973  hashdvds  12980  phimullem  12984  eulerthlemth  12991  prmdiveq  12995  prmdivdiv  12996  pythagtriplem4  13028  pythagtriplem10  13029  pythagtriplem19  13042  pcpre1  13052  pcadd2  13101  qexpz  13112  expnprm  13113  oddprmdvds  13114  pockthlem  13116  4sqlem7  13144  4sqlem10  13147  4sqexercise1  13158  4sqexercise2  13159  4sqlemsdc  13160  4sqlem11  13161  4sqlem12  13162  4sqlem14  13164  4sqlem15  13165  4sqlem16  13166  ennnfonelemkh  13284  ennnfonelemnn0  13294  qusgrp  14015  dvdsrid  14383  dvdsrtr  14384  dvdsrneg  14386  unitmulcl  14396  unitgrp  14399  unitnegcl  14413  subrguss  14520  subrgunit  14523  znidomb  14968  psmetsym  15356  psmettri  15357  mettri2  15389  xmetsym  15395  xmettri  15399  metrtri  15404  xblss2ps  15431  xblss2  15432  blhalf  15435  xmsge0  15494  cnmet  15557  ivthinclemlopn  15663  ivthdichlem  15678  dveflem  15753  dvef  15754  plyaddlem1  15774  sin0pilem1  15808  sinq12gt0  15857  sinq34lt0t  15858  cosq14gt0  15859  coseq0q4123  15861  rpabscxpbnd  15968  logbgcd1irraplemexp  15996  dvdsppwf1o  16020  mpodvdsmulf1o  16021  perfectlem2  16031  lgslem1  16036  lgseisenlem2  16107  lgsquadlem1  16113  lgsquadlem2  16114  lgsquad2lem1  16117  2sqlem3  16153  2sqlem4  16154  2sqlem8  16159  dichmul0orlem1  16670  pwf1oexmid  16946  qdencn  16980  cvgcmp2nlemabs  16989  apdifflemf  17003  apdifflemr  17004