Theorem breqtrd 4044

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

Syntax hints:   -> wi 4   = wceq 1364   class class class wbr 4018

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-un 3148  df-sn 3613  df-pr 3614  df-op 3616  df-br 4019

This theorem is referenced by:  breqtrrd  4046  breqtrid  4055  tfrexlem  6358  phplem4  6882  phplem4on  6894  fidifsnen  6897  fisbth  6910  fin0  6912  fin0or  6913  ltsonq  7426  addlocprlemeqgt  7560  prmuloclemcalc  7593  mullocprlem  7598  addcanprlemu  7643  ltaprlem  7646  ltaprg  7647  prplnqu  7648  ltmprr  7670  cauappcvgprlemopl  7674  cauappcvgprlemloc  7680  cauappcvgprlemladdru  7684  cauappcvgprlemladdrl  7685  cauappcvgprlem1  7687  caucvgprlemm  7696  caucvgprlemopl  7697  caucvgprlemloc  7703  caucvgprprlemloccalc  7712  caucvgprprlemopl  7725  recexgt0sr  7801  ltm1sr  7805  prsrpos  7813  caucvgsrlemoffgt1  7827  caucvgsr  7830  suplocsrlempr  7835  pitoregt0  7877  axpre-suploclemres  7929  add20  8460  mullt0  8466  ltmul1a  8577  ltm1  8832  recgt0  8836  prodgt0gt0  8837  prodgt0  8838  prodge0  8840  lemul1a  8844  recp1lt1  8885  recreclt  8886  ledivp1  8889  mulle0r  8930  ltaddrp2d  9760  mul2lt0np  9792  xleadd1a  9902  xleaddadd  9916  fz01en  10082  fzonmapblen  10216  qbtwnrelemcalc  10285  flqaddz  10327  flhalf  10332  flqdiv  10351  modqmuladdim  10397  modqsubdir  10423  addmodlteq  10428  frecfzen2  10457  iseqf1olemab  10519  ser3le  10548  ltexp2a  10602  leexp2a  10603  exple1  10606  expubnd  10607  bernneq  10671  faclbnd6  10755  hashfz  10832  zfz1isolemiso  10850  zfz1iso  10852  seq3coll  10853  cvg1nlemcxze  11022  cvg1nlemres  11025  recvguniqlem  11034  resqrexlemover  11050  resqrexlemdec  11051  resqrexlemcalc2  11055  resqrexlemcalc3  11056  resqrexlemnm  11058  resqrexlemoverl  11061  ltabs  11127  abslt  11128  absle  11129  abstri  11144  maxabslemlub  11247  maxabslemval  11248  dfabsmax  11257  bdtrilem  11278  xrmaxiflemab  11286  xrmaxiflemlub  11287  xrmaxaddlem  11299  reccn2ap  11352  climge0  11364  climaddc2  11369  summodclem2a  11420  zsumdc  11423  isumge0  11469  fsumle  11502  fsumlt  11503  isumshft  11529  expcnvap0  11541  geolim  11550  geolim2  11551  georeclim  11552  geo2lim  11555  cvgratnnlembern  11562  cvgratnnlemfm  11568  mertenslemi1  11574  mertensabs  11576  prodmodclem3  11614  prodmodclem2a  11615  zproddc  11618  fprodseq  11622  efcllemp  11697  ef0lem  11699  efgt0  11723  eftlub  11729  efltim  11737  sinbnd  11791  cosbnd  11792  ef01bndlem  11795  sin01gt0  11800  cos01gt0  11801  sin02gt0  11802  eirraplem  11815  dvdssub2  11873  dvdsadd2b  11878  dvdsexp  11898  opoe  11931  divalglemeunn  11957  divalglemex  11958  divalglemeuneg  11959  gcdaddm  12016  bezoutlemstep  12029  dvdsgcd  12044  dvdsmulgcd  12057  bezoutr1  12065  nn0seqcvgd  12072  rpmulgcd2  12126  qredeq  12127  rpdvds  12130  prmind2  12151  divdenle  12228  phicl2  12245  hashdvds  12252  phimullem  12256  eulerthlemth  12263  prmdiveq  12267  prmdivdiv  12268  pythagtriplem4  12299  pythagtriplem10  12300  pythagtriplem19  12313  pcpre1  12323  pcadd2  12372  qexpz  12383  expnprm  12384  oddprmdvds  12385  pockthlem  12387  4sqlem7  12415  4sqlem10  12418  4sqexercise1  12429  4sqexercise2  12430  4sqlemsdc  12431  4sqlem11  12432  4sqlem12  12433  4sqlem14  12435  4sqlem15  12436  4sqlem16  12437  ennnfonelemkh  12462  ennnfonelemnn0  12472  qusgrp  13168  dvdsrid  13447  dvdsrtr  13448  dvdsrneg  13450  unitmulcl  13460  unitgrp  13463  unitnegcl  13477  subrguss  13580  subrgunit  13583  psmetsym  14281  psmettri  14282  mettri2  14314  xmetsym  14320  xmettri  14324  metrtri  14329  xblss2ps  14356  xblss2  14357  blhalf  14360  xmsge0  14419  cnmet  14482  ivthinclemlopn  14566  dveflem  14639  dvef  14640  sin0pilem1  14654  sinq12gt0  14703  sinq34lt0t  14704  cosq14gt0  14705  coseq0q4123  14707  rpabscxpbnd  14811  logbgcd1irraplemexp  14838  lgslem1  14854  lgseisenlem2  14904  2sqlem3  14917  2sqlem4  14918  2sqlem8  14923  pwf1oexmid  15203  qdencn  15229  cvgcmp2nlemabs  15234  apdifflemf  15248  apdifflemr  15249