Theorem breqtrd 3844

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

Syntax hints:   -> wi 4   = wceq 1287   class class class wbr 3820

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-un 2992  df-sn 3437  df-pr 3438  df-op 3440  df-br 3821

This theorem is referenced by:  breqtrrd  3846  syl5breq  3855  tfrexlem  6053  phplem4  6523  phplem4on  6535  fidifsnen  6538  fisbth  6551  fin0  6553  fin0or  6554  ltsonq  6901  addlocprlemeqgt  7035  prmuloclemcalc  7068  mullocprlem  7073  addcanprlemu  7118  ltaprlem  7121  ltaprg  7122  prplnqu  7123  ltmprr  7145  cauappcvgprlemopl  7149  cauappcvgprlemloc  7155  cauappcvgprlemladdru  7159  cauappcvgprlemladdrl  7160  cauappcvgprlem1  7162  caucvgprlemm  7171  caucvgprlemopl  7172  caucvgprlemloc  7178  caucvgprprlemloccalc  7187  caucvgprprlemopl  7200  recexgt0sr  7263  prsrpos  7274  caucvgsrlemoffgt1  7288  caucvgsr  7291  pitoregt0  7330  add20  7896  mullt0  7902  ltmul1a  8009  ltm1  8242  recgt0  8246  prodgt0gt0  8247  prodgt0  8248  prodge0  8250  lemul1a  8254  recp1lt1  8295  recreclt  8296  ledivp1  8299  mulle0r  8340  ltaddrp2d  9140  fz01en  9399  fzonmapblen  9526  qbtwnrelemcalc  9595  flqaddz  9632  flhalf  9637  flqdiv  9656  modqmuladdim  9702  modqsubdir  9728  addmodlteq  9733  frecfzen2  9762  iseqf1olemab  9823  serile  9852  ltexp2a  9906  leexp2a  9907  exple1  9910  expubnd  9911  bernneq  9971  faclbnd6  10049  hashfz  10126  zfz1isolemiso  10141  zfz1iso  10143  iseqcoll  10144  cvg1nlemcxze  10311  cvg1nlemres  10314  recvguniqlem  10323  resqrexlemover  10339  resqrexlemdec  10340  resqrexlemcalc2  10344  resqrexlemcalc3  10345  resqrexlemnm  10347  resqrexlemoverl  10350  ltabs  10416  abslt  10417  absle  10418  abstri  10433  maxabslemlub  10536  maxabslemval  10537  dfabsmax  10546  climge0  10607  climaddc2  10612  isummolem2a  10662  zisum  10665  dvdssub2  10720  dvdsadd2b  10725  dvdsexp  10744  opoe  10777  divalglemeunn  10803  divalglemex  10804  divalglemeuneg  10805  gcdaddm  10857  bezoutlemstep  10868  dvdsgcd  10883  dvdsmulgcd  10896  bezoutr1  10904  nn0seqcvgd  10905  rpmulgcd2  10959  qredeq  10960  rpdvds  10963  prmind2  10984  divdenle  11057  phicl2  11072  hashdvds  11079  phimullem  11083  qdencn  11360