Theorem 3brtr3d 3896

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

Syntax hints:   → wi 4   = wceq 1296   class class class wbr 3867

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-3an 929  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-v 2635  df-un 3017  df-sn 3472  df-pr 3473  df-op 3475  df-br 3868

This theorem is referenced by:  ofrval  5904  phplem2  6649  ltaddnq  7063  prarloclemarch2  7075  prmuloclemcalc  7221  axcaucvglemcau  7530  apreap  8161  ltmul1  8166  subap0d  8216  divap1d  8365  div2subap  8399  lemul2a  8417  xleadd2a  9440  monoord2  10043  expubnd  10143  bernneq2  10206  resqrexlemcalc2  10579  resqrexlemcalc3  10580  abs2dif2  10671  bdtrilem  10801  bdtri  10802  xrmaxaddlem  10819  fsum00  11020  iserabs  11033  geosergap  11064  mertenslemi1  11093  eftlub  11144  eirraplem  11228  xblss2  12206  xmstri2  12271  mstri2  12272  xmstri  12273  mstri  12274  xmstri3  12275  mstri3  12276  msrtri  12277