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  7765  addlocprlemeqgt  7899  prmuloclemcalc  7932  mullocprlem  7937  addcanprlemu  7982  ltaprlem  7985  ltaprg  7986  prplnqu  7987  ltmprr  8009  cauappcvgprlemopl  8013  cauappcvgprlemloc  8019  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  cauappcvgprlem1  8026  caucvgprlemm  8035  caucvgprlemopl  8036  caucvgprlemloc  8042  caucvgprprlemloccalc  8051  caucvgprprlemopl  8064  recexgt0sr  8140  ltm1sr  8144  prsrpos  8152  caucvgsrlemoffgt1  8166  caucvgsr  8169  suplocsrlempr  8174  pitoregt0  8216  axpre-suploclemres  8268  add20  8802  mullt0  8808  ltmul1a  8919  ltm1  9176  recgt0  9180  prodgt0gt0  9181  prodgt0  9182  prodge0  9184  lemul1a  9188  recp1lt1  9229  recreclt  9230  ledivp1  9233  mulle0r  9274  eluzmn  9928  ltaddrp2d  10132  mul2lt0np  10164  xleadd1a  10275  xleaddadd  10289  lincmble  10406  fz01en  10459  fzonmapblen  10599  qbtwnrelemcalc  10690  flqaddz  10732  flhalf  10737  flqdiv  10758  modqmuladdim  10804  modqsubdir  10830  addmodlteq  10835  frecfzen2  10864  iseqf1olemab  10939  ser3le  10974  ltexp2a  11028  leexp2a  11029  exple1  11032  expubnd  11033  bernneq  11098  faclbnd6  11182  hashfz  11262  zfz1isolemiso  11291  zfz1iso  11293  seq3coll  11294  cvg1nlemcxze  11748  cvg1nlemres  11751  recvguniqlem  11760  resqrexlemover  11776  resqrexlemdec  11777  resqrexlemcalc2  11781  resqrexlemcalc3  11782  resqrexlemnm  11784  resqrexlemoverl  11787  ltabs  11853  abslt  11854  absle  11855  abstri  11870  maxabslemlub  11973  maxabslemval  11974  dfabsmax  11983  bdtrilem  12005  xrmaxiflemab  12013  xrmaxiflemlub  12014  xrmaxaddlem  12026  reccn2ap  12079  climge0  12091  climaddc2  12096  summodclem2a  12148  zsumdc  12151  isumge0  12197  fsumle  12230  fsumlt  12231  isumshft  12257  expcnvap0  12269  geolim  12278  geolim2  12279  georeclim  12280  geo2lim  12283  cvgratnnlembern  12290  cvgratnnlemfm  12296  mertenslemi1  12302  mertensabs  12304  prodmodclem3  12342  prodmodclem2a  12343  zproddc  12346  fprodseq  12350  efcllemp  12425  ef0lem  12427  efgt0  12451  eftlub  12457  efltim  12465  sinbnd  12519  cosbnd  12520  ef01bndlem  12523  sin01gt0  12529  cos01gt0  12530  sin02gt0  12531  eirraplem  12544  dvdssub2  12602  dvdsadd2b  12607  dvdsexp  12628  3dvds  12631  opoe  12662  divalglemeunn  12688  divalglemex  12689  divalglemeuneg  12690  bitsfzolem  12721  bitsinv1lem  12728  gcdaddm  12761  bezoutlemstep  12774  dvdsgcd  12789  dvdsmulgcd  12802  bezoutr1  12810  nninfctlemfo  12817  nn0seqcvgd  12819  rpmulgcd2  12873  qredeq  12874  rpdvds  12877  prmind2  12898  divdenle  12975  phicl2  12992  hashdvds  12999  phimullem  13003  eulerthlemth  13010  prmdiveq  13014  prmdivdiv  13015  pythagtriplem4  13047  pythagtriplem10  13048  pythagtriplem19  13061  pcpre1  13071  pcadd2  13120  qexpz  13131  expnprm  13132  oddprmdvds  13133  pockthlem  13135  4sqlem7  13163  4sqlem10  13166  4sqexercise1  13177  4sqexercise2  13178  4sqlemsdc  13179  4sqlem11  13180  4sqlem12  13181  4sqlem14  13183  4sqlem15  13184  4sqlem16  13185  ennnfonelemkh  13303  ennnfonelemnn0  13313  qusgrp  14035  dvdsrid  14407  dvdsrtr  14408  dvdsrneg  14410  unitmulcl  14420  unitgrp  14423  unitnegcl  14437  subrguss  14544  subrgunit  14547  znidomb  14993  psmetsym  15430  psmettri  15431  mettri2  15463  xmetsym  15469  xmettri  15473  metrtri  15478  xblss2ps  15505  xblss2  15506  blhalf  15509  xmsge0  15568  cnmet  15631  ivthinclemlopn  15737  ivthdichlem  15752  dveflem  15827  dvef  15828  plyaddlem1  15848  sin0pilem1  15882  sinq12gt0  15931  sinq34lt0t  15932  cosq14gt0  15933  coseq0q4123  15935  rpabscxpbnd  16042  logbgcd1irraplemexp  16070  log2tlbndlog2  16082  birthdaylem2  16088  birthdaylem3  16089  dvdsppwf1o  16103  mpodvdsmulf1o  16104  perfectlem2  16114  lgslem1  16119  lgseisenlem2  16190  lgsquadlem1  16196  lgsquadlem2  16197  lgsquad2lem1  16200  2sqlem3  16236  2sqlem4  16237  2sqlem8  16242  dichmul0orlem1  16753  pwf1oexmid  17029  qdencn  17072  cvgcmp2nlemabs  17081  apdifflemf  17095  apdifflemr  17096