Theorem breqtrd 3954

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

Syntax hints:   -> wi 4   = wceq 1331   class class class wbr 3929

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536  df-br 3930

This theorem is referenced by:  breqtrrd  3956  breqtrid  3965  tfrexlem  6231  phplem4  6749  phplem4on  6761  fidifsnen  6764  fisbth  6777  fin0  6779  fin0or  6780  ltsonq  7206  addlocprlemeqgt  7340  prmuloclemcalc  7373  mullocprlem  7378  addcanprlemu  7423  ltaprlem  7426  ltaprg  7427  prplnqu  7428  ltmprr  7450  cauappcvgprlemopl  7454  cauappcvgprlemloc  7460  cauappcvgprlemladdru  7464  cauappcvgprlemladdrl  7465  cauappcvgprlem1  7467  caucvgprlemm  7476  caucvgprlemopl  7477  caucvgprlemloc  7483  caucvgprprlemloccalc  7492  caucvgprprlemopl  7505  recexgt0sr  7581  ltm1sr  7585  prsrpos  7593  caucvgsrlemoffgt1  7607  caucvgsr  7610  suplocsrlempr  7615  pitoregt0  7657  axpre-suploclemres  7709  add20  8236  mullt0  8242  ltmul1a  8353  ltm1  8604  recgt0  8608  prodgt0gt0  8609  prodgt0  8610  prodge0  8612  lemul1a  8616  recp1lt1  8657  recreclt  8658  ledivp1  8661  mulle0r  8702  ltaddrp2d  9518  mul2lt0np  9550  xleadd1a  9656  xleaddadd  9670  fz01en  9833  fzonmapblen  9964  qbtwnrelemcalc  10033  flqaddz  10070  flhalf  10075  flqdiv  10094  modqmuladdim  10140  modqsubdir  10166  addmodlteq  10171  frecfzen2  10200  iseqf1olemab  10262  ser3le  10291  ltexp2a  10345  leexp2a  10346  exple1  10349  expubnd  10350  bernneq  10412  faclbnd6  10490  hashfz  10567  zfz1isolemiso  10582  zfz1iso  10584  seq3coll  10585  cvg1nlemcxze  10754  cvg1nlemres  10757  recvguniqlem  10766  resqrexlemover  10782  resqrexlemdec  10783  resqrexlemcalc2  10787  resqrexlemcalc3  10788  resqrexlemnm  10790  resqrexlemoverl  10793  ltabs  10859  abslt  10860  absle  10861  abstri  10876  maxabslemlub  10979  maxabslemval  10980  dfabsmax  10989  bdtrilem  11010  xrmaxiflemab  11016  xrmaxiflemlub  11017  xrmaxaddlem  11029  reccn2ap  11082  climge0  11094  climaddc2  11099  summodclem2a  11150  zsumdc  11153  isumge0  11199  fsumle  11232  fsumlt  11233  isumshft  11259  expcnvap0  11271  geolim  11280  geolim2  11281  georeclim  11282  geo2lim  11285  cvgratnnlembern  11292  cvgratnnlemfm  11298  mertenslemi1  11304  mertensabs  11306  prodmodclem3  11344  prodmodclem2a  11345  efcllemp  11364  ef0lem  11366  efgt0  11390  eftlub  11396  efltim  11404  sinbnd  11459  cosbnd  11460  ef01bndlem  11463  sin01gt0  11468  cos01gt0  11469  sin02gt0  11470  eirraplem  11483  dvdssub2  11535  dvdsadd2b  11540  dvdsexp  11559  opoe  11592  divalglemeunn  11618  divalglemex  11619  divalglemeuneg  11620  gcdaddm  11672  bezoutlemstep  11685  dvdsgcd  11700  dvdsmulgcd  11713  bezoutr1  11721  nn0seqcvgd  11722  rpmulgcd2  11776  qredeq  11777  rpdvds  11780  prmind2  11801  divdenle  11875  phicl2  11890  hashdvds  11897  phimullem  11901  ennnfonelemkh  11925  ennnfonelemnn0  11935  psmetsym  12498  psmettri  12499  mettri2  12531  xmetsym  12537  xmettri  12541  metrtri  12546  xblss2ps  12573  xblss2  12574  blhalf  12577  xmsge0  12636  cnmet  12699  ivthinclemlopn  12783  dveflem  12855  dvef  12856  sin0pilem1  12862  sinq12gt0  12911  sinq34lt0t  12912  cosq14gt0  12913  coseq0q4123  12915  pwf1oexmid  13194  qdencn  13222  cvgcmp2nlemabs  13227