Theorem 3brtr3d 4036

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

Syntax hints:   -> wi 4   = wceq 1353   class class class wbr 4005

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2741  df-un 3135  df-sn 3600  df-pr 3601  df-op 3603  df-br 4006

This theorem is referenced by:  ofrval  6095  phplem2  6855  ltaddnq  7408  prarloclemarch2  7420  prmuloclemcalc  7566  axcaucvglemcau  7899  apreap  8546  ltmul1  8551  divap1d  8760  div2subap  8796  lemul2a  8818  mul2lt0rlt0  9761  xleadd2a  9876  monoord2  10479  expubnd  10579  bernneq2  10644  nn0ltexp2  10691  apexp1  10700  resqrexlemcalc2  11026  resqrexlemcalc3  11027  abs2dif2  11118  bdtrilem  11249  bdtri  11250  xrmaxaddlem  11270  fsum00  11472  iserabs  11485  geosergap  11516  mertenslemi1  11545  eftlub  11700  eirraplem  11786  unitmulcl  13287  unitgrp  13290  xblss2  13990  xmstri2  14055  mstri2  14056  xmstri  14057  mstri  14058  xmstri3  14059  mstri3  14060  msrtri  14061  logdivlti  14387  2sqlem8  14555  apdifflemr  14880