Theorem 3brtr4d 3841

Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 21-Feb-2005.)

Hypotheses

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

Assertion

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

Proof of Theorem 3brtr4d

Step	Hyp	Ref	Expression
1		3brtr4d.1	. 2 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		3brtr4d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐴)
3		3brtr4d.3	. . 3 ⊢ (𝜑 → 𝐷 = 𝐵)
4	2, 3	breq12d 3824	. 2 ⊢ (𝜑 → (𝐶𝑅𝐷 ↔ 𝐴𝑅𝐵))
5	1, 4	mpbird 165	1 ⊢ (𝜑 → 𝐶𝑅𝐷)

Syntax hints:   → wi 4   = wceq 1285   class class class wbr 3811

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065

This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-v 2614  df-un 2988  df-sn 3428  df-pr 3429  df-op 3431  df-br 3812

This theorem is referenced by:  f1oiso2  5545  prarloclemarch2  6881  caucvgprprlemmu  7157  caucvgsrlembound  7242  mulap0  8021  lediv12a  8249  recp1lt1  8254  fldiv4p1lem1div2  9601  intfracq  9616  modqmulnn  9638  addmodlteq  9694  frecfzennn  9722  monoord2  9771  expgt1  9830  leexp2r  9846  leexp1a  9847  bernneq  9909  faclbnd  9984  faclbnd6  9987  facubnd  9988  hashunlem  10047  sqrtgt0  10294  absrele  10343  absimle  10344  abstri  10364  abs2difabs  10368  climsqz  10547  climsqz2  10548  phibnd  10973