Theorem 3brtr3d 4117

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 4099	. 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 4086

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 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-br 4087

This theorem is referenced by:  ofrval  6241  phplem2  7034  ltaddnq  7617  prarloclemarch2  7629  prmuloclemcalc  7775  axcaucvglemcau  8108  apreap  8757  ltmul1  8762  divap1d  8971  div2subap  9007  lemul2a  9029  mul2lt0rlt0  9984  xleadd2a  10099  monoord2  10738  expubnd  10848  bernneq2  10913  nn0ltexp2  10961  apexp1  10970  resqrexlemcalc2  11566  resqrexlemcalc3  11567  abs2dif2  11658  bdtrilem  11790  bdtri  11791  xrmaxaddlem  11811  fsum00  12013  iserabs  12026  geosergap  12057  mertenslemi1  12086  eftlub  12241  eirraplem  12328  bitscmp  12509  unitmulcl  14117  unitgrp  14120  xblss2  15119  xmstri2  15184  mstri2  15185  xmstri  15186  mstri  15187  xmstri3  15188  mstri3  15189  msrtri  15190  logdivlti  15595  perfectlem2  15714  2sqlem8  15842  apdifflemr  16587