Theorem 3brtr3d 4119

Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 18-Oct-1999.)

Hypotheses

Ref	Expression
3brtr3d.1	|- ( ph -> A R B )
3brtr3d.2	|- ( ph -> A = C )
3brtr3d.3	|- ( ph -> B = D )

Assertion

Ref	Expression
3brtr3d	|- ( ph -> C R D )

Proof of Theorem 3brtr3d

Step	Hyp	Ref	Expression
1		3brtr3d.1	. 2 |- ( ph -> A R B )
2		3brtr3d.2	. . 3 |- ( ph -> A = C )
3		3brtr3d.3	. . 3 |- ( ph -> B = D )
4	2, 3	breq12d 4101	. 2 |- ( ph -> ( A R B <-> C R D ) )
5	1, 4	mpbid 147	1 |- ( ph -> C R D )

Syntax hints:   -> wi 4   = wceq 1397   class class class wbr 4088

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-br 4089

This theorem is referenced by:  ofrval  6245  phplem2  7038  ltaddnq  7626  prarloclemarch2  7638  prmuloclemcalc  7784  axcaucvglemcau  8117  apreap  8766  ltmul1  8771  divap1d  8980  div2subap  9016  lemul2a  9038  mul2lt0rlt0  9993  xleadd2a  10108  monoord2  10747  expubnd  10857  bernneq2  10922  nn0ltexp2  10970  apexp1  10979  resqrexlemcalc2  11575  resqrexlemcalc3  11576  abs2dif2  11667  bdtrilem  11799  bdtri  11800  xrmaxaddlem  11820  fsum00  12022  iserabs  12035  geosergap  12066  mertenslemi1  12095  eftlub  12250  eirraplem  12337  bitscmp  12518  unitmulcl  14126  unitgrp  14129  xblss2  15128  xmstri2  15193  mstri2  15194  xmstri  15195  mstri  15196  xmstri3  15197  mstri3  15198  msrtri  15199  logdivlti  15604  perfectlem2  15723  2sqlem8  15851  apdifflemr  16651