Theorem 3brtr4d 4118

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

Syntax hints:   → wi 4   = wceq 1395   class class class wbr 4086

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-br 4087

This theorem is referenced by:  f1oiso2  5963  prarloclemarch2  7629  caucvgprprlemmu  7905  caucvgsrlembound  8004  mulap0  8824  lediv12a  9064  recp1lt1  9069  xleadd1a  10098  fldiv4p1lem1div2  10555  fldiv4lem1div2  10557  intfracq  10572  modqmulnn  10594  addmodlteq  10650  frecfzennn  10678  monoord2  10738  expgt1  10829  leexp2r  10845  leexp1a  10846  bernneq  10912  faclbnd  10993  faclbnd6  10996  facubnd  10997  hashunlem  11057  zfz1isolemiso  11093  sqrtgt0  11585  absrele  11634  absimle  11635  abstri  11655  abs2difabs  11659  bdtrilem  11790  bdtri  11791  xrmaxifle  11797  xrmaxadd  11812  xrbdtri  11827  climsqz  11886  climsqz2  11887  fsum3cvg2  11945  isumle  12046  expcnvap0  12053  expcnvre  12054  explecnv  12056  cvgratz  12083  efcllemp  12209  ege2le3  12222  eflegeo  12252  cos12dec  12319  fsumdvds  12393  phibnd  12779  pcdvdstr  12890  pcprmpw2  12896  pockthg  12920  2expltfac  13002  znrrg  14664  psmetres2  15047  xmetres2  15093  comet  15213  bdxmet  15215  cnmet  15244  ivthdec  15358  limcimolemlt  15378  tangtx  15552  logbgcd1irraplemap  15683  2lgslem1c  15809  cvgcmp2nlemabs  16572  trilpolemlt1  16581