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  13944  xmstri2  14009  mstri2  14010  xmstri  14011  mstri  14012  xmstri3  14013  mstri3  14014  msrtri  14015  logdivlti  14341  2sqlem8  14509  apdifflemr  14834