Theorem breqtrrd 4159

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)

Hypotheses

Ref	Expression
breqtrrd.1	|- ( ph -> A R B )
breqtrrd.2	|- ( ph -> C = B )

Assertion

Ref	Expression
breqtrrd	|- ( ph -> A R C )

Proof of Theorem breqtrrd

Step	Hyp	Ref	Expression
1		breqtrrd.1	. 2 |- ( ph -> A R B )
2		breqtrrd.2	. . 3 |- ( ph -> C = B )
3	2	eqcomd 2244	. 2 |- ( ph -> B = C )
4	1, 3	breqtrd 4157	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:  frirrg  4497  fidcen  7209  unsnfidcex  7233  unsnfidcel  7234  addlocprlemeq  7906  ltexprlemopl  7974  recexprlemloc  8004  cauappcvgprlemopl  8019  cauappcvgprlemladdfu  8027  cauappcvgprlem1  8032  caucvgprlemopl  8042  caucvgprlemladdfu  8050  caucvgprprlemopl  8070  caucvgprprlemexbt  8079  mulgt0sr  8151  archsr  8155  caucvgsrlemoffgt1  8172  suplocsrlemb  8179  suplocsrlem  8181  mulap0r  8951  prodgt0  9190  div4p1lem1div2  9570  mul2lt0rgt0  10177  xnn0dcle  10220  xnn0letri  10221  xleadd1a  10291  xltadd1  10294  xlt2add  10298  xposdif  10300  xlesubadd  10301  xleaddadd  10305  uzsubsubfz  10468  fzctr  10556  subfzo0  10677  exbtwnzlemstep  10698  exbtwnzlemex  10700  rebtwn2zlemstep  10703  rebtwn2z  10705  qbtwnxr  10708  xqltnle  10718  fldiv4lem1div2uz2  10761  ceilqge  10767  modqge0  10789  modqlt  10790  modqid  10806  m1modge3gt1  10828  modaddmodup  10844  addmodlteq  10855  ser3mono  10944  seqf1oglem1  10976  seqf1oglem2  10977  ser3ge0  10993  ser3le  10994  leexp1a  11051  sqgt0ap  11065  sqge0  11073  nnlesq  11100  expnbnd  11121  nn0sqdc  11167  nn0opthlem2d  11180  facwordi  11199  bcm1n  11228  filtinf  11251  hashunlem  11265  zfz1isolemiso  11312  cats1fvd  11559  cjmulge0  11675  resqrexlemover  11797  resqrexlemdec  11798  resqrexlemlo  11800  resqrexlemcalc3  11803  resqrexlemcvg  11806  resqrexlemoverl  11808  resqrexlemglsq  11809  resqrexlemga  11810  absge0  11847  amgm2  11906  maxle1  11999  bdtrilem  12029  xrmaxifle  12036  xrmaxiflemlub  12038  xrmaxiflemval  12040  xrmax1sup  12043  xrmaxltsup  12048  xrmaxadd  12051  xrbdtri  12066  reccn2ap  12103  climle  12124  climserle  12135  isumclim2  12213  isumclim3  12214  isumge0  12221  fsumlessfi  12251  expcnvap0  12293  expcnvre  12294  explecnv  12296  absltap  12300  cvgratnnlembern  12314  cvgratnnlemnexp  12315  cvgratnnlemmn  12316  cvgratnnlemabsle  12318  cvgratnnlemfm  12320  cvgratnnlemrate  12321  mertenslemi1  12326  mertenslem2  12327  clim2divap  12331  prodmodclem3  12366  efcvg  12457  ege2le3  12462  efaddlem  12465  eftlub  12481  effsumlt  12483  ef01bndlem  12547  sin02gt0  12555  eirrap  12569  iddvdsexp  12606  dvdsadd  12627  dvdsfac  12651  dvdsmod  12653  3dvds  12655  omoe  12687  divalglemnn  12709  divalglemnqt  12711  flodddiv4t2lthalf  12730  bitsfzo  12746  bitsmod  12747  bitscmp  12749  bitsinv1lem  12752  dvdslegcd  12765  dfgcd3  12811  dvdssqim  12825  dvdsmulgcd  12826  nn0seqcvgd  12843  dvdslcm  12871  lcmgcdlem  12879  mulgcddvds  12896  qredeq  12898  cncongr2  12906  sqnprm  12939  isprm6  12950  sqpweven  12979  znege1  12982  sqrt2irrap  12984  nonsq  13011  hashdvds  13027  prmdiv  13041  odzdvds  13052  pythagtriplem4  13075  pcpre1  13099  pcdvdsb  13127  pcz  13139  pcprmpw2  13140  pcaddlem  13146  pcadd  13147  pcadd2  13148  pcmpt  13150  pcmptdvds  13152  fldivp1  13155  pcfaclem  13156  pockthlem  13163  4sqlem6  13190  4sqlem8  13192  4sqexercise1  13205  4sqexercise2  13206  4sqlemsdc  13207  4sqlem11  13208  4sqlem12  13209  4sqlem14  13211  4sqlem16  13213  ballotfilemsgt1  13311  ballotfilemsel1i  13313  ennnfonelemkh  13360  nninfdclemp1  13398  eqgen  14088  dvdsrmul1  14517  unitmulclb  14529  subrguss  14652  znidom  15100  znunit  15102  psrbagmaxlem1x  15181  psrbagmaxlem1y  15182  psmetxrge0  15575  isxmet2d  15591  mettri  15616  xmettri3  15617  mettri3  15618  xblss2ps  15647  blss2ps  15649  blss2  15650  blssps  15670  blss  15671  xmetxp  15750  ivthdec  15887  ivthreinc  15888  hoverb  15891  hovergt0  15893  sin0pilem1  16025  sinq12gt0  16074  tangtx  16082  cosordlem  16094  cosq34lt1  16095  logdivlti  16128  logbgcd1irrap  16223  birthdaylem3  16244  chtqge0  16264  chtublem  16312  perfectlem1  16316  bcmax  16322  bposlem1  16328  bposlem2  16329  bposlem5  16332  bposlem6  16333  bposlem7  16334  lgsdilem2  16377  gausslemma2dlem1f1o  16401  lgsquadlem1  16418  2lgsoddprmlem2  16447  2sqlem3  16458  2sqlem8  16464  usgrsizedgen  16676  cvgcmp2nlemabs  17304  trilpolemclim  17309  trilpolemeq1  17313  apdifflemf  17319  apdifflemr  17320  nconstwlpolemgt0  17338