Theorem 3brtr3d 4018

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

Syntax hints:   -> wi 4   = wceq 1348   class class class wbr 3987

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-sn 3587  df-pr 3588  df-op 3590  df-br 3988

This theorem is referenced by:  ofrval  6068  phplem2  6827  ltaddnq  7356  prarloclemarch2  7368  prmuloclemcalc  7514  axcaucvglemcau  7847  apreap  8493  ltmul1  8498  divap1d  8705  div2subap  8741  lemul2a  8762  mul2lt0rlt0  9703  xleadd2a  9818  monoord2  10420  expubnd  10520  bernneq2  10584  nn0ltexp2  10631  apexp1  10639  resqrexlemcalc2  10966  resqrexlemcalc3  10967  abs2dif2  11058  bdtrilem  11189  bdtri  11190  xrmaxaddlem  11210  fsum00  11412  iserabs  11425  geosergap  11456  mertenslemi1  11485  eftlub  11640  eirraplem  11726  xblss2  13158  xmstri2  13223  mstri2  13224  xmstri  13225  mstri  13226  xmstri3  13227  mstri3  13228  msrtri  13229  logdivlti  13555  2sqlem8  13712  apdifflemr  14039