Theorem breqtrd 4013

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

Syntax hints:   -> wi 4   = wceq 1348   class class class wbr 3987

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-sn 3587  df-pr 3588  df-op 3590  df-br 3988

This theorem is referenced by:  breqtrrd  4015  breqtrid  4024  tfrexlem  6310  phplem4  6829  phplem4on  6841  fidifsnen  6844  fisbth  6857  fin0  6859  fin0or  6860  ltsonq  7347  addlocprlemeqgt  7481  prmuloclemcalc  7514  mullocprlem  7519  addcanprlemu  7564  ltaprlem  7567  ltaprg  7568  prplnqu  7569  ltmprr  7591  cauappcvgprlemopl  7595  cauappcvgprlemloc  7601  cauappcvgprlemladdru  7605  cauappcvgprlemladdrl  7606  cauappcvgprlem1  7608  caucvgprlemm  7617  caucvgprlemopl  7618  caucvgprlemloc  7624  caucvgprprlemloccalc  7633  caucvgprprlemopl  7646  recexgt0sr  7722  ltm1sr  7726  prsrpos  7734  caucvgsrlemoffgt1  7748  caucvgsr  7751  suplocsrlempr  7756  pitoregt0  7798  axpre-suploclemres  7850  add20  8380  mullt0  8386  ltmul1a  8497  ltm1  8749  recgt0  8753  prodgt0gt0  8754  prodgt0  8755  prodge0  8757  lemul1a  8761  recp1lt1  8802  recreclt  8803  ledivp1  8806  mulle0r  8847  ltaddrp2d  9675  mul2lt0np  9707  xleadd1a  9817  xleaddadd  9831  fz01en  9996  fzonmapblen  10130  qbtwnrelemcalc  10199  flqaddz  10240  flhalf  10245  flqdiv  10264  modqmuladdim  10310  modqsubdir  10336  addmodlteq  10341  frecfzen2  10370  iseqf1olemab  10432  ser3le  10461  ltexp2a  10515  leexp2a  10516  exple1  10519  expubnd  10520  bernneq  10583  faclbnd6  10665  hashfz  10743  zfz1isolemiso  10761  zfz1iso  10763  seq3coll  10764  cvg1nlemcxze  10933  cvg1nlemres  10936  recvguniqlem  10945  resqrexlemover  10961  resqrexlemdec  10962  resqrexlemcalc2  10966  resqrexlemcalc3  10967  resqrexlemnm  10969  resqrexlemoverl  10972  ltabs  11038  abslt  11039  absle  11040  abstri  11055  maxabslemlub  11158  maxabslemval  11159  dfabsmax  11168  bdtrilem  11189  xrmaxiflemab  11197  xrmaxiflemlub  11198  xrmaxaddlem  11210  reccn2ap  11263  climge0  11275  climaddc2  11280  summodclem2a  11331  zsumdc  11334  isumge0  11380  fsumle  11413  fsumlt  11414  isumshft  11440  expcnvap0  11452  geolim  11461  geolim2  11462  georeclim  11463  geo2lim  11466  cvgratnnlembern  11473  cvgratnnlemfm  11479  mertenslemi1  11485  mertensabs  11487  prodmodclem3  11525  prodmodclem2a  11526  zproddc  11529  fprodseq  11533  efcllemp  11608  ef0lem  11610  efgt0  11634  eftlub  11640  efltim  11648  sinbnd  11702  cosbnd  11703  ef01bndlem  11706  sin01gt0  11711  cos01gt0  11712  sin02gt0  11713  eirraplem  11726  dvdssub2  11784  dvdsadd2b  11789  dvdsexp  11808  opoe  11841  divalglemeunn  11867  divalglemex  11868  divalglemeuneg  11869  gcdaddm  11926  bezoutlemstep  11939  dvdsgcd  11954  dvdsmulgcd  11967  bezoutr1  11975  nn0seqcvgd  11982  rpmulgcd2  12036  qredeq  12037  rpdvds  12040  prmind2  12061  divdenle  12138  phicl2  12155  hashdvds  12162  phimullem  12166  eulerthlemth  12173  prmdiveq  12177  prmdivdiv  12178  pythagtriplem4  12209  pythagtriplem10  12210  pythagtriplem19  12223  pcpre1  12233  qexpz  12291  expnprm  12292  oddprmdvds  12293  pockthlem  12295  4sqlem7  12323  4sqlem10  12326  ennnfonelemkh  12354  ennnfonelemnn0  12364  psmetsym  13044  psmettri  13045  mettri2  13077  xmetsym  13083  xmettri  13087  metrtri  13092  xblss2ps  13119  xblss2  13120  blhalf  13123  xmsge0  13182  cnmet  13245  ivthinclemlopn  13329  dveflem  13402  dvef  13403  sin0pilem1  13417  sinq12gt0  13466  sinq34lt0t  13467  cosq14gt0  13468  coseq0q4123  13470  rpabscxpbnd  13574  logbgcd1irraplemexp  13601  lgslem1  13616  2sqlem3  13668  2sqlem4  13669  2sqlem8  13674  pwf1oexmid  13954  qdencn  13981  cvgcmp2nlemabs  13986  apdifflemf  14000  apdifflemr  14001