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  8803  mullt0  8809  ltmul1a  8921  ltm1  9178  recgt0  9182  prodgt0gt0  9183  prodgt0  9184  prodge0  9186  lemul1a  9190  recp1lt1  9231  recreclt  9232  ledivp1  9235  mulle0r  9276  eluzmn  9937  irraddap  10056  ltaddrp2d  10142  mul2lt0np  10174  xleadd1a  10285  xleaddadd  10299  lincmble  10416  fz01en  10469  fzonmapblen  10609  qbtwnrelemcalc  10700  flqaddz  10745  flhalf  10750  flqdiv  10771  modqmuladdim  10817  modqsubdir  10843  addmodlteq  10848  frecfzen2  10877  iseqf1olemab  10952  ser3le  10987  ltexp2a  11041  leexp2a  11042  exple1  11045  expubnd  11046  bernneq  11111  faclbnd6  11196  hashfz  11276  zfz1isolemiso  11305  zfz1iso  11307  seq3coll  11308  cvg1nlemcxze  11762  cvg1nlemres  11765  recvguniqlem  11774  resqrexlemover  11790  resqrexlemdec  11791  resqrexlemcalc2  11795  resqrexlemcalc3  11796  resqrexlemnm  11798  resqrexlemoverl  11801  ltabs  11868  abslt  11869  absle  11870  abstri  11885  maxabslemlub  11988  maxabslemval  11989  dfabsmax  11998  bdtrilem  12021  xrmaxiflemab  12029  xrmaxiflemlub  12030  xrmaxaddlem  12042  reccn2ap  12095  climge0  12107  climaddc2  12112  summodclem2a  12164  zsumdc  12167  isumge0  12213  fsumle  12246  fsumlt  12247  isumshft  12273  expcnvap0  12285  geolim  12294  geolim2  12295  georeclim  12296  geo2lim  12299  cvgratnnlembern  12306  cvgratnnlemfm  12312  mertenslemi1  12318  mertensabs  12320  prodmodclem3  12358  prodmodclem2a  12359  zproddc  12362  fprodseq  12366  efcllemp  12441  ef0lem  12443  efgt0  12467  eftlub  12473  efltim  12481  sinbnd  12535  cosbnd  12536  ef01bndlem  12539  sin01gt0  12545  cos01gt0  12546  sin02gt0  12547  eirraplem  12560  dvdssub2  12618  dvdsadd2b  12623  dvdsexp  12644  3dvds  12647  opoe  12678  divalglemeunn  12704  divalglemex  12705  divalglemeuneg  12706  bitsfzolem  12737  bitsinv1lem  12744  gcdaddm  12777  bezoutlemstep  12790  dvdsgcd  12805  dvdsmulgcd  12818  bezoutr1  12826  nninfctlemfo  12833  nn0seqcvgd  12835  rpmulgcd2  12889  qredeq  12890  rpdvds  12893  prmind2  12914  divdenle  12993  phicl2  13012  hashdvds  13019  phimullem  13023  eulerthlemth  13030  prmdiveq  13034  prmdivdiv  13035  pythagtriplem4  13067  pythagtriplem10  13068  pythagtriplem19  13081  pcpre1  13091  pcadd2  13140  qexpz  13151  expnprm  13152  oddprmdvds  13153  pockthlem  13155  4sqlem7  13183  4sqlem10  13186  4sqexercise1  13197  4sqexercise2  13198  4sqlemsdc  13199  4sqlem11  13200  4sqlem12  13201  4sqlem14  13203  4sqlem15  13204  4sqlem16  13205  ennnfonelemkh  13352  ennnfonelemnn0  13362  qusgrp  14084  dvdsrid  14456  dvdsrtr  14457  dvdsrneg  14459  unitmulcl  14469  unitgrp  14472  unitnegcl  14486  subrguss  14593  subrgunit  14596  znidomb  15042  psmetsym  15479  psmettri  15480  mettri2  15512  xmetsym  15518  xmettri  15522  metrtri  15527  xblss2ps  15554  xblss2  15555  blhalf  15558  xmsge0  15617  cnmet  15680  ivthinclemlopn  15786  ivthdichlem  15801  dveflem  15876  dvef  15877  plyaddlem1  15897  sin0pilem1  15932  sinq12gt0  15981  sinq34lt0t  15982  cosq14gt0  15983  coseq0q4123  15985  logdivlt  16046  rpabscxpbnd  16095  logbgcd1irraplemexp  16123  log2tlbndlog2  16139  birthdaylem2  16145  birthdaylem3  16146  dvdsppwf1o  16184  mpodvdsmulf1o  16185  perfectlem2  16198  bclbnd  16205  bposlem1  16209  bposlem3  16211  bposlem4  16212  lgslem1  16217  lgseisenlem2  16288  lgsquadlem1  16294  lgsquadlem2  16295  lgsquad2lem1  16298  2sqlem3  16334  2sqlem4  16335  2sqlem8  16340  dichmul0orlem1  16851  pwf1oexmid  17127  qdencn  17170  cvgcmp2nlemabs  17179  apdifflemf  17193  apdifflemr  17194