Theorem breqtrd 4156

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 4142	. 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 4130

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 4131

This theorem is used by:  breqtrrd  4158  breqtrid  4167  tfrexlem  6605  phplem4  7156  phplem4on  7169  fidifsnen  7172  fisbth  7187  fin0  7189  fin0or  7190  ltsonq  7766  addlocprlemeqgt  7900  prmuloclemcalc  7933  mullocprlem  7938  addcanprlemu  7983  ltaprlem  7986  ltaprg  7987  prplnqu  7988  ltmprr  8010  cauappcvgprlemopl  8014  cauappcvgprlemloc  8020  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  cauappcvgprlem1  8027  caucvgprlemm  8036  caucvgprlemopl  8037  caucvgprlemloc  8043  caucvgprprlemloccalc  8052  caucvgprprlemopl  8065  recexgt0sr  8141  ltm1sr  8145  prsrpos  8153  caucvgsrlemoffgt1  8167  caucvgsr  8170  suplocsrlempr  8175  pitoregt0  8217  axpre-suploclemres  8269  add20  8804  mullt0  8810  ltmul1a  8922  ltm1  9179  recgt0  9183  prodgt0gt0  9184  prodgt0  9185  prodge0  9187  lemul1a  9191  recp1lt1  9232  recreclt  9233  ledivp1  9236  mulle0r  9277  eluzmn  9938  irraddap  10057  ltaddrp2d  10143  mul2lt0np  10175  xleadd1a  10286  xleaddadd  10300  lincmble  10417  fz01en  10470  fzonmapblen  10610  qbtwnrelemcalc  10701  flqaddz  10747  flhalf  10752  flqdiv  10773  modqmuladdim  10819  modqsubdir  10845  addmodlteq  10850  frecfzen2  10879  iseqf1olemab  10954  ser3le  10989  ltexp2a  11043  leexp2a  11044  exple1  11047  expubnd  11048  bernneq  11113  faclbnd6  11198  hashfz  11278  zfz1isolemiso  11307  zfz1iso  11309  seq3coll  11310  cvg1nlemcxze  11764  cvg1nlemres  11767  recvguniqlem  11776  resqrexlemover  11792  resqrexlemdec  11793  resqrexlemcalc2  11797  resqrexlemcalc3  11798  resqrexlemnm  11800  resqrexlemoverl  11803  ltabs  11870  abslt  11871  absle  11872  abstri  11887  maxabslemlub  11990  maxabslemval  11991  dfabsmax  12000  bdtrilem  12024  xrmaxiflemab  12032  xrmaxiflemlub  12033  xrmaxaddlem  12045  reccn2ap  12098  climge0  12110  climaddc2  12115  summodclem2a  12167  zsumdc  12170  isumge0  12216  fsumle  12249  fsumlt  12250  isumshft  12276  expcnvap0  12288  geolim  12297  geolim2  12298  georeclim  12299  geo2lim  12302  cvgratnnlembern  12309  cvgratnnlemfm  12315  mertenslemi1  12321  mertensabs  12323  prodmodclem3  12361  prodmodclem2a  12362  zproddc  12365  fprodseq  12369  efcllemp  12444  ef0lem  12446  efgt0  12470  eftlub  12476  efltim  12484  sinbnd  12538  cosbnd  12539  ef01bndlem  12542  sin01gt0  12548  cos01gt0  12549  sin02gt0  12550  eirraplem  12563  dvdssub2  12621  dvdsadd2b  12626  dvdsexp  12647  3dvds  12650  opoe  12681  divalglemeunn  12707  divalglemex  12708  divalglemeuneg  12709  bitsfzolem  12740  bitsinv1lem  12747  gcdaddm  12780  bezoutlemstep  12793  dvdsgcd  12808  dvdsmulgcd  12821  bezoutr1  12829  nninfctlemfo  12836  nn0seqcvgd  12838  rpmulgcd2  12892  qredeq  12893  rpdvds  12896  prmind2  12917  divdenle  12996  phicl2  13015  hashdvds  13022  phimullem  13026  eulerthlemth  13033  prmdiveq  13037  prmdivdiv  13038  pythagtriplem4  13070  pythagtriplem10  13071  pythagtriplem19  13084  pcpre1  13094  pcadd2  13143  qexpz  13154  expnprm  13155  oddprmdvds  13156  pockthlem  13158  4sqlem7  13186  4sqlem10  13189  4sqexercise1  13200  4sqexercise2  13201  4sqlemsdc  13202  4sqlem11  13203  4sqlem12  13204  4sqlem14  13206  4sqlem15  13207  4sqlem16  13208  ennnfonelemkh  13355  ennnfonelemnn0  13365  qusgrp  14088  dvdsrid  14491  dvdsrtr  14492  dvdsrneg  14494  unitmulcl  14504  unitgrp  14507  unitnegcl  14521  subrguss  14628  subrgunit  14631  znidomb  15077  psmetsym  15521  psmettri  15522  mettri2  15554  xmetsym  15560  xmettri  15564  metrtri  15569  xblss2ps  15596  xblss2  15597  blhalf  15600  xmsge0  15659  cnmet  15722  ivthinclemlopn  15828  ivthdichlem  15843  dveflem  15918  dvef  15919  plyaddlem1  15939  sin0pilem1  15974  sinq12gt0  16023  sinq34lt0t  16024  cosq14gt0  16025  coseq0q4123  16027  logdivlt  16088  rpabscxpbnd  16137  logbgcd1irraplemexp  16165  log2tlbndlog2  16181  birthdaylem2  16187  birthdaylem3  16188  dvdsppwf1o  16244  mpodvdsmulf1o  16245  chtqub  16257  perfectlem2  16261  bclbnd  16268  bposlem1  16272  bposlem3  16274  bposlem4  16275  bposlem6  16277  lgslem1  16285  lgseisenlem2  16356  lgsquadlem1  16362  lgsquadlem2  16363  lgsquad2lem1  16366  2sqlem3  16402  2sqlem4  16403  2sqlem8  16408  dichmul0orlem1  16919  pwf1oexmid  17195  qdencn  17238  cvgcmp2nlemabs  17247  apdifflemf  17262  apdifflemr  17263