Theorem breqtrd 4109

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

Syntax hints:   -> wi 4   = wceq 1395   class class class wbr 4083

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-br 4084

This theorem is referenced by:  breqtrrd  4111  breqtrid  4120  tfrexlem  6486  phplem4  7024  phplem4on  7037  fidifsnen  7040  fisbth  7053  fin0  7055  fin0or  7056  ltsonq  7596  addlocprlemeqgt  7730  prmuloclemcalc  7763  mullocprlem  7768  addcanprlemu  7813  ltaprlem  7816  ltaprg  7817  prplnqu  7818  ltmprr  7840  cauappcvgprlemopl  7844  cauappcvgprlemloc  7850  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  cauappcvgprlem1  7857  caucvgprlemm  7866  caucvgprlemopl  7867  caucvgprlemloc  7873  caucvgprprlemloccalc  7882  caucvgprprlemopl  7895  recexgt0sr  7971  ltm1sr  7975  prsrpos  7983  caucvgsrlemoffgt1  7997  caucvgsr  8000  suplocsrlempr  8005  pitoregt0  8047  axpre-suploclemres  8099  add20  8632  mullt0  8638  ltmul1a  8749  ltm1  9004  recgt0  9008  prodgt0gt0  9009  prodgt0  9010  prodge0  9012  lemul1a  9016  recp1lt1  9057  recreclt  9058  ledivp1  9061  mulle0r  9102  eluzmn  9740  ltaddrp2d  9939  mul2lt0np  9971  xleadd1a  10081  xleaddadd  10095  fz01en  10261  fzonmapblen  10399  qbtwnrelemcalc  10487  flqaddz  10529  flhalf  10534  flqdiv  10555  modqmuladdim  10601  modqsubdir  10627  addmodlteq  10632  frecfzen2  10661  iseqf1olemab  10736  ser3le  10771  ltexp2a  10825  leexp2a  10826  exple1  10829  expubnd  10830  bernneq  10894  faclbnd6  10978  hashfz  11056  zfz1isolemiso  11074  zfz1iso  11076  seq3coll  11077  cvg1nlemcxze  11509  cvg1nlemres  11512  recvguniqlem  11521  resqrexlemover  11537  resqrexlemdec  11538  resqrexlemcalc2  11542  resqrexlemcalc3  11543  resqrexlemnm  11545  resqrexlemoverl  11548  ltabs  11614  abslt  11615  absle  11616  abstri  11631  maxabslemlub  11734  maxabslemval  11735  dfabsmax  11744  bdtrilem  11766  xrmaxiflemab  11774  xrmaxiflemlub  11775  xrmaxaddlem  11787  reccn2ap  11840  climge0  11852  climaddc2  11857  summodclem2a  11908  zsumdc  11911  isumge0  11957  fsumle  11990  fsumlt  11991  isumshft  12017  expcnvap0  12029  geolim  12038  geolim2  12039  georeclim  12040  geo2lim  12043  cvgratnnlembern  12050  cvgratnnlemfm  12056  mertenslemi1  12062  mertensabs  12064  prodmodclem3  12102  prodmodclem2a  12103  zproddc  12106  fprodseq  12110  efcllemp  12185  ef0lem  12187  efgt0  12211  eftlub  12217  efltim  12225  sinbnd  12279  cosbnd  12280  ef01bndlem  12283  sin01gt0  12289  cos01gt0  12290  sin02gt0  12291  eirraplem  12304  dvdssub2  12362  dvdsadd2b  12367  dvdsexp  12388  3dvds  12391  opoe  12422  divalglemeunn  12448  divalglemex  12449  divalglemeuneg  12450  bitsfzolem  12481  bitsinv1lem  12488  gcdaddm  12521  bezoutlemstep  12534  dvdsgcd  12549  dvdsmulgcd  12562  bezoutr1  12570  nninfctlemfo  12577  nn0seqcvgd  12579  rpmulgcd2  12633  qredeq  12634  rpdvds  12637  prmind2  12658  divdenle  12735  phicl2  12752  hashdvds  12759  phimullem  12763  eulerthlemth  12770  prmdiveq  12774  prmdivdiv  12775  pythagtriplem4  12807  pythagtriplem10  12808  pythagtriplem19  12821  pcpre1  12831  pcadd2  12880  qexpz  12891  expnprm  12892  oddprmdvds  12893  pockthlem  12895  4sqlem7  12923  4sqlem10  12926  4sqexercise1  12937  4sqexercise2  12938  4sqlemsdc  12939  4sqlem11  12940  4sqlem12  12941  4sqlem14  12943  4sqlem15  12944  4sqlem16  12945  ennnfonelemkh  12999  ennnfonelemnn0  13009  qusgrp  13785  dvdsrid  14080  dvdsrtr  14081  dvdsrneg  14083  unitmulcl  14093  unitgrp  14096  unitnegcl  14110  subrguss  14216  subrgunit  14219  znidomb  14638  psmetsym  15019  psmettri  15020  mettri2  15052  xmetsym  15058  xmettri  15062  metrtri  15067  xblss2ps  15094  xblss2  15095  blhalf  15098  xmsge0  15157  cnmet  15220  ivthinclemlopn  15326  ivthdichlem  15341  dveflem  15416  dvef  15417  plyaddlem1  15437  sin0pilem1  15471  sinq12gt0  15520  sinq34lt0t  15521  cosq14gt0  15522  coseq0q4123  15524  rpabscxpbnd  15630  logbgcd1irraplemexp  15658  dvdsppwf1o  15679  mpodvdsmulf1o  15680  perfectlem2  15690  lgslem1  15695  lgseisenlem2  15766  lgsquadlem1  15772  lgsquadlem2  15773  lgsquad2lem1  15776  2sqlem3  15812  2sqlem4  15813  2sqlem8  15818  pwf1oexmid  16452  qdencn  16483  cvgcmp2nlemabs  16488  apdifflemf  16502  apdifflemr  16503