Theorem 3brtr3d 4079

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

Syntax hints:   → wi 4   = wceq 1373   class class class wbr 4048

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 2188

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-un 3172  df-sn 3641  df-pr 3642  df-op 3644  df-br 4049

This theorem is referenced by:  ofrval  6179  phplem2  6962  ltaddnq  7533  prarloclemarch2  7545  prmuloclemcalc  7691  axcaucvglemcau  8024  apreap  8673  ltmul1  8678  divap1d  8887  div2subap  8923  lemul2a  8945  mul2lt0rlt0  9894  xleadd2a  10009  monoord2  10644  expubnd  10754  bernneq2  10819  nn0ltexp2  10867  apexp1  10876  resqrexlemcalc2  11376  resqrexlemcalc3  11377  abs2dif2  11468  bdtrilem  11600  bdtri  11601  xrmaxaddlem  11621  fsum00  11823  iserabs  11836  geosergap  11867  mertenslemi1  11896  eftlub  12051  eirraplem  12138  bitscmp  12319  unitmulcl  13925  unitgrp  13928  xblss2  14927  xmstri2  14992  mstri2  14993  xmstri  14994  mstri  14995  xmstri3  14996  mstri3  14997  msrtri  14998  logdivlti  15403  perfectlem2  15522  2sqlem8  15650  apdifflemr  16101