Theorem breqtrd 4109

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

Syntax hints:   -> wi 4   = wceq 1395   class class class wbr 4083

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-br 4084

This theorem is referenced by:  breqtrrd  4111  breqtrid  4120  tfrexlem  6480  phplem4  7016  phplem4on  7029  fidifsnen  7032  fisbth  7045  fin0  7047  fin0or  7048  ltsonq  7585  addlocprlemeqgt  7719  prmuloclemcalc  7752  mullocprlem  7757  addcanprlemu  7802  ltaprlem  7805  ltaprg  7806  prplnqu  7807  ltmprr  7829  cauappcvgprlemopl  7833  cauappcvgprlemloc  7839  cauappcvgprlemladdru  7843  cauappcvgprlemladdrl  7844  cauappcvgprlem1  7846  caucvgprlemm  7855  caucvgprlemopl  7856  caucvgprlemloc  7862  caucvgprprlemloccalc  7871  caucvgprprlemopl  7884  recexgt0sr  7960  ltm1sr  7964  prsrpos  7972  caucvgsrlemoffgt1  7986  caucvgsr  7989  suplocsrlempr  7994  pitoregt0  8036  axpre-suploclemres  8088  add20  8621  mullt0  8627  ltmul1a  8738  ltm1  8993  recgt0  8997  prodgt0gt0  8998  prodgt0  8999  prodge0  9001  lemul1a  9005  recp1lt1  9046  recreclt  9047  ledivp1  9050  mulle0r  9091  ltaddrp2d  9927  mul2lt0np  9959  xleadd1a  10069  xleaddadd  10083  fz01en  10249  fzonmapblen  10387  qbtwnrelemcalc  10475  flqaddz  10517  flhalf  10522  flqdiv  10543  modqmuladdim  10589  modqsubdir  10615  addmodlteq  10620  frecfzen2  10649  iseqf1olemab  10724  ser3le  10759  ltexp2a  10813  leexp2a  10814  exple1  10817  expubnd  10818  bernneq  10882  faclbnd6  10966  hashfz  11043  zfz1isolemiso  11061  zfz1iso  11063  seq3coll  11064  cvg1nlemcxze  11493  cvg1nlemres  11496  recvguniqlem  11505  resqrexlemover  11521  resqrexlemdec  11522  resqrexlemcalc2  11526  resqrexlemcalc3  11527  resqrexlemnm  11529  resqrexlemoverl  11532  ltabs  11598  abslt  11599  absle  11600  abstri  11615  maxabslemlub  11718  maxabslemval  11719  dfabsmax  11728  bdtrilem  11750  xrmaxiflemab  11758  xrmaxiflemlub  11759  xrmaxaddlem  11771  reccn2ap  11824  climge0  11836  climaddc2  11841  summodclem2a  11892  zsumdc  11895  isumge0  11941  fsumle  11974  fsumlt  11975  isumshft  12001  expcnvap0  12013  geolim  12022  geolim2  12023  georeclim  12024  geo2lim  12027  cvgratnnlembern  12034  cvgratnnlemfm  12040  mertenslemi1  12046  mertensabs  12048  prodmodclem3  12086  prodmodclem2a  12087  zproddc  12090  fprodseq  12094  efcllemp  12169  ef0lem  12171  efgt0  12195  eftlub  12201  efltim  12209  sinbnd  12263  cosbnd  12264  ef01bndlem  12267  sin01gt0  12273  cos01gt0  12274  sin02gt0  12275  eirraplem  12288  dvdssub2  12346  dvdsadd2b  12351  dvdsexp  12372  3dvds  12375  opoe  12406  divalglemeunn  12432  divalglemex  12433  divalglemeuneg  12434  bitsfzolem  12465  bitsinv1lem  12472  gcdaddm  12505  bezoutlemstep  12518  dvdsgcd  12533  dvdsmulgcd  12546  bezoutr1  12554  nninfctlemfo  12561  nn0seqcvgd  12563  rpmulgcd2  12617  qredeq  12618  rpdvds  12621  prmind2  12642  divdenle  12719  phicl2  12736  hashdvds  12743  phimullem  12747  eulerthlemth  12754  prmdiveq  12758  prmdivdiv  12759  pythagtriplem4  12791  pythagtriplem10  12792  pythagtriplem19  12805  pcpre1  12815  pcadd2  12864  qexpz  12875  expnprm  12876  oddprmdvds  12877  pockthlem  12879  4sqlem7  12907  4sqlem10  12910  4sqexercise1  12921  4sqexercise2  12922  4sqlemsdc  12923  4sqlem11  12924  4sqlem12  12925  4sqlem14  12927  4sqlem15  12928  4sqlem16  12929  ennnfonelemkh  12983  ennnfonelemnn0  12993  qusgrp  13769  dvdsrid  14064  dvdsrtr  14065  dvdsrneg  14067  unitmulcl  14077  unitgrp  14080  unitnegcl  14094  subrguss  14200  subrgunit  14203  znidomb  14622  psmetsym  15003  psmettri  15004  mettri2  15036  xmetsym  15042  xmettri  15046  metrtri  15051  xblss2ps  15078  xblss2  15079  blhalf  15082  xmsge0  15141  cnmet  15204  ivthinclemlopn  15310  ivthdichlem  15325  dveflem  15400  dvef  15401  plyaddlem1  15421  sin0pilem1  15455  sinq12gt0  15504  sinq34lt0t  15505  cosq14gt0  15506  coseq0q4123  15508  rpabscxpbnd  15614  logbgcd1irraplemexp  15642  dvdsppwf1o  15663  mpodvdsmulf1o  15664  perfectlem2  15674  lgslem1  15679  lgseisenlem2  15750  lgsquadlem1  15756  lgsquadlem2  15757  lgsquad2lem1  15760  2sqlem3  15796  2sqlem4  15797  2sqlem8  15802  pwf1oexmid  16365  qdencn  16395  cvgcmp2nlemabs  16400  apdifflemf  16414  apdifflemr  16415