Theorem 3brtr3d 4114

Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 18-Oct-1999.)

Hypotheses

Ref	Expression
3brtr3d.1	⊢ (𝜑 → 𝐴𝑅𝐵)
3brtr3d.2	⊢ (𝜑 → 𝐴 = 𝐶)
3brtr3d.3	⊢ (𝜑 → 𝐵 = 𝐷)

Assertion

Ref	Expression
3brtr3d	⊢ (𝜑 → 𝐶𝑅𝐷)

Proof of Theorem 3brtr3d

Step	Hyp	Ref	Expression
1		3brtr3d.1	. 2 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		3brtr3d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐶)
3		3brtr3d.3	. . 3 ⊢ (𝜑 → 𝐵 = 𝐷)
4	2, 3	breq12d 4096	. 2 ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐶𝑅𝐷))
5	1, 4	mpbid 147	1 ⊢ (𝜑 → 𝐶𝑅𝐷)

Syntax hints:   → wi 4   = wceq 1395   class class class wbr 4083

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-br 4084

This theorem is referenced by:  ofrval  6235  phplem2  7022  ltaddnq  7602  prarloclemarch2  7614  prmuloclemcalc  7760  axcaucvglemcau  8093  apreap  8742  ltmul1  8747  divap1d  8956  div2subap  8992  lemul2a  9014  mul2lt0rlt0  9963  xleadd2a  10078  monoord2  10716  expubnd  10826  bernneq2  10891  nn0ltexp2  10939  apexp1  10948  resqrexlemcalc2  11534  resqrexlemcalc3  11535  abs2dif2  11626  bdtrilem  11758  bdtri  11759  xrmaxaddlem  11779  fsum00  11981  iserabs  11994  geosergap  12025  mertenslemi1  12054  eftlub  12209  eirraplem  12296  bitscmp  12477  unitmulcl  14085  unitgrp  14088  xblss2  15087  xmstri2  15152  mstri2  15153  xmstri  15154  mstri  15155  xmstri3  15156  mstri3  15157  msrtri  15158  logdivlti  15563  perfectlem2  15682  2sqlem8  15810  apdifflemr  16445