Theorem 3brtr3d 4074

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

Syntax hints:   -> wi 4   = wceq 1372   class class class wbr 4043

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-un 3169  df-sn 3638  df-pr 3639  df-op 3641  df-br 4044

This theorem is referenced by:  ofrval  6168  phplem2  6949  ltaddnq  7519  prarloclemarch2  7531  prmuloclemcalc  7677  axcaucvglemcau  8010  apreap  8659  ltmul1  8664  divap1d  8873  div2subap  8909  lemul2a  8931  mul2lt0rlt0  9880  xleadd2a  9995  monoord2  10629  expubnd  10739  bernneq2  10804  nn0ltexp2  10852  apexp1  10861  resqrexlemcalc2  11297  resqrexlemcalc3  11298  abs2dif2  11389  bdtrilem  11521  bdtri  11522  xrmaxaddlem  11542  fsum00  11744  iserabs  11757  geosergap  11788  mertenslemi1  11817  eftlub  11972  eirraplem  12059  bitscmp  12240  unitmulcl  13846  unitgrp  13849  xblss2  14848  xmstri2  14913  mstri2  14914  xmstri  14915  mstri  14916  xmstri3  14917  mstri3  14918  msrtri  14919  logdivlti  15324  perfectlem2  15443  2sqlem8  15571  apdifflemr  15948