Theorem breqtrd 3788

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

Syntax hints:   -> wi 4   = wceq 1243   class class class wbr 3764

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-v 2559  df-un 2922  df-sn 3381  df-pr 3382  df-op 3384  df-br 3765

This theorem is referenced by:  breqtrrd  3790  syl5breq  3799  tfrexlem  5948  phplem4  6318  phplem4on  6329  fidifsnen  6331  fisbth  6340  fin0  6342  fin0or  6343  ltsonq  6496  addlocprlemeqgt  6630  prmuloclemcalc  6663  mullocprlem  6668  addcanprlemu  6713  ltaprlem  6716  ltaprg  6717  prplnqu  6718  ltmprr  6740  cauappcvgprlemopl  6744  cauappcvgprlemloc  6750  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  cauappcvgprlem1  6757  caucvgprlemm  6766  caucvgprlemopl  6767  caucvgprlemloc  6773  caucvgprprlemloccalc  6782  caucvgprprlemopl  6795  recexgt0sr  6858  prsrpos  6869  caucvgsrlemoffgt1  6883  caucvgsr  6886  pitoregt0  6925  add20  7469  mullt0  7475  ltmul1a  7582  ltm1  7812  recgt0  7816  prodgt0gt0  7817  prodgt0  7818  prodge0  7820  lemul1a  7824  recp1lt1  7865  recreclt  7866  ledivp1  7869  ltaddrp2d  8657  fz01en  8917  fzonmapblen  9043  qbtwnrelemcalc  9110  flqaddz  9139  flhalf  9144  flqdiv  9163  frecfzen2  9204  serile  9253  ltexp2a  9306  leexp2a  9307  exple1  9310  expubnd  9311  bernneq  9369  cvg1nlemcxze  9581  cvg1nlemres  9584  recvguniqlem  9592  resqrexlemover  9608  resqrexlemdec  9609  resqrexlemcalc2  9613  resqrexlemcalc3  9614  resqrexlemnm  9616  resqrexlemoverl  9619  ltabs  9683  abslt  9684  absle  9685  abstri  9700  climge0  9845  climaddc2  9850  nn0seqcvgd  9880  qdencn  10124