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  6238  phplem2  7027  ltaddnq  7610  prarloclemarch2  7622  prmuloclemcalc  7768  axcaucvglemcau  8101  apreap  8750  ltmul1  8755  divap1d  8964  div2subap  9000  lemul2a  9022  mul2lt0rlt0  9972  xleadd2a  10087  monoord2  10725  expubnd  10835  bernneq2  10900  nn0ltexp2  10948  apexp1  10957  resqrexlemcalc2  11547  resqrexlemcalc3  11548  abs2dif2  11639  bdtrilem  11771  bdtri  11772  xrmaxaddlem  11792  fsum00  11994  iserabs  12007  geosergap  12038  mertenslemi1  12067  eftlub  12222  eirraplem  12309  bitscmp  12490  unitmulcl  14098  unitgrp  14101  xblss2  15100  xmstri2  15165  mstri2  15166  xmstri  15167  mstri  15168  xmstri3  15169  mstri3  15170  msrtri  15171  logdivlti  15576  perfectlem2  15695  2sqlem8  15823  apdifflemr  16529