Theorem 3brtr4d 4120

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

Syntax hints:   → wi 4   = wceq 1397   class class class wbr 4088

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-br 4089

This theorem is referenced by:  f1oiso2  5968  prarloclemarch2  7639  caucvgprprlemmu  7915  caucvgsrlembound  8014  mulap0  8834  lediv12a  9074  recp1lt1  9079  xleadd1a  10108  fldiv4p1lem1div2  10566  fldiv4lem1div2  10568  intfracq  10583  modqmulnn  10605  addmodlteq  10661  frecfzennn  10689  monoord2  10749  expgt1  10840  leexp2r  10856  leexp1a  10857  bernneq  10923  faclbnd  11004  faclbnd6  11007  facubnd  11008  hashunlem  11068  zfz1isolemiso  11104  sqrtgt0  11599  absrele  11648  absimle  11649  abstri  11669  abs2difabs  11673  bdtrilem  11804  bdtri  11805  xrmaxifle  11811  xrmaxadd  11826  xrbdtri  11841  climsqz  11900  climsqz2  11901  fsum3cvg2  11960  isumle  12061  expcnvap0  12068  expcnvre  12069  explecnv  12071  cvgratz  12098  efcllemp  12224  ege2le3  12237  eflegeo  12267  cos12dec  12334  fsumdvds  12408  phibnd  12794  pcdvdstr  12905  pcprmpw2  12911  pockthg  12935  2expltfac  13017  znrrg  14680  psmetres2  15063  xmetres2  15109  comet  15229  bdxmet  15231  cnmet  15260  ivthdec  15374  limcimolemlt  15394  tangtx  15568  logbgcd1irraplemap  15699  2lgslem1c  15825  cvgcmp2nlemabs  16662  trilpolemlt1  16671