Theorem 3brtr3d 4117

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 4099	. 2 ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐶𝑅𝐷))
5	1, 4	mpbid 147	1 ⊢ (𝜑 → 𝐶𝑅𝐷)

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

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 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-br 4087

This theorem is referenced by:  ofrval  6241  phplem2  7034  ltaddnq  7620  prarloclemarch2  7632  prmuloclemcalc  7778  axcaucvglemcau  8111  apreap  8760  ltmul1  8765  divap1d  8974  div2subap  9010  lemul2a  9032  mul2lt0rlt0  9987  xleadd2a  10102  monoord2  10741  expubnd  10851  bernneq2  10916  nn0ltexp2  10964  apexp1  10973  resqrexlemcalc2  11569  resqrexlemcalc3  11570  abs2dif2  11661  bdtrilem  11793  bdtri  11794  xrmaxaddlem  11814  fsum00  12016  iserabs  12029  geosergap  12060  mertenslemi1  12089  eftlub  12244  eirraplem  12331  bitscmp  12512  unitmulcl  14120  unitgrp  14123  xblss2  15122  xmstri2  15187  mstri2  15188  xmstri  15189  mstri  15190  xmstri3  15191  mstri3  15192  msrtri  15193  logdivlti  15598  perfectlem2  15717  2sqlem8  15845  apdifflemr  16601