Theorem 3brtr4d 3897

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 3880	. 2 ⊢ (𝜑 → (𝐶𝑅𝐷 ↔ 𝐴𝑅𝐵))
5	1, 4	mpbird 166	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:  f1oiso2  5644  prarloclemarch2  7075  caucvgprprlemmu  7351  caucvgsrlembound  7436  mulap0  8220  lediv12a  8452  recp1lt1  8457  xleadd1a  9439  fldiv4p1lem1div2  9861  intfracq  9876  modqmulnn  9898  addmodlteq  9954  frecfzennn  9982  monoord2  10027  expgt1  10108  leexp2r  10124  leexp1a  10125  bernneq  10189  faclbnd  10264  faclbnd6  10267  facubnd  10268  hashunlem  10327  zfz1isolemiso  10359  sqrtgt0  10582  absrele  10631  absimle  10632  abstri  10652  abs2difabs  10656  bdtrilem  10785  bdtri  10786  xrmaxifle  10789  xrmaxadd  10804  xrbdtri  10819  climsqz  10878  climsqz2  10879  fsum3cvg2  10937  isumle  11038  expcnvap0  11045  expcnvre  11046  explecnv  11048  cvgratz  11075  efcllemp  11097  ege2le3  11110  eflegeo  11141  phibnd  11620  psmetres2  12119  xmetres2  12165  comet  12285  bdxmet  12287  cnmet  12309