Theorem 3brtr3d 4091

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

Syntax hints:   -> wi 4   = wceq 1373   class class class wbr 4060

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2779  df-un 3179  df-sn 3650  df-pr 3651  df-op 3653  df-br 4061

This theorem is referenced by:  ofrval  6194  phplem2  6977  ltaddnq  7557  prarloclemarch2  7569  prmuloclemcalc  7715  axcaucvglemcau  8048  apreap  8697  ltmul1  8702  divap1d  8911  div2subap  8947  lemul2a  8969  mul2lt0rlt0  9918  xleadd2a  10033  monoord2  10670  expubnd  10780  bernneq2  10845  nn0ltexp2  10893  apexp1  10902  resqrexlemcalc2  11487  resqrexlemcalc3  11488  abs2dif2  11579  bdtrilem  11711  bdtri  11712  xrmaxaddlem  11732  fsum00  11934  iserabs  11947  geosergap  11978  mertenslemi1  12007  eftlub  12162  eirraplem  12249  bitscmp  12430  unitmulcl  14036  unitgrp  14039  xblss2  15038  xmstri2  15103  mstri2  15104  xmstri  15105  mstri  15106  xmstri3  15107  mstri3  15108  msrtri  15109  logdivlti  15514  perfectlem2  15633  2sqlem8  15761  apdifflemr  16296