Theorem 3brtr3d 4114

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

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:  ofrval  6235  phplem2  7022  ltaddnq  7605  prarloclemarch2  7617  prmuloclemcalc  7763  axcaucvglemcau  8096  apreap  8745  ltmul1  8750  divap1d  8959  div2subap  8995  lemul2a  9017  mul2lt0rlt0  9967  xleadd2a  10082  monoord2  10720  expubnd  10830  bernneq2  10895  nn0ltexp2  10943  apexp1  10952  resqrexlemcalc2  11541  resqrexlemcalc3  11542  abs2dif2  11633  bdtrilem  11765  bdtri  11766  xrmaxaddlem  11786  fsum00  11988  iserabs  12001  geosergap  12032  mertenslemi1  12061  eftlub  12216  eirraplem  12303  bitscmp  12484  unitmulcl  14092  unitgrp  14095  xblss2  15094  xmstri2  15159  mstri2  15160  xmstri  15161  mstri  15162  xmstri3  15163  mstri3  15164  msrtri  15165  logdivlti  15570  perfectlem2  15689  2sqlem8  15817  apdifflemr  16479