Theorem 3brtr4d 4125

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

Syntax hints:   → wi 4   = wceq 1398   class class class wbr 4093

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-br 4094

This theorem is referenced by:  f1oiso2  5978  prarloclemarch2  7682  caucvgprprlemmu  7958  caucvgsrlembound  8057  mulap0  8876  lediv12a  9116  recp1lt1  9121  xleadd1a  10152  fldiv4p1lem1div2  10611  fldiv4lem1div2  10613  intfracq  10628  modqmulnn  10650  addmodlteq  10706  frecfzennn  10734  monoord2  10794  expgt1  10885  leexp2r  10901  leexp1a  10902  bernneq  10968  faclbnd  11049  faclbnd6  11052  facubnd  11053  hashunlem  11113  zfz1isolemiso  11149  sqrtgt0  11657  absrele  11706  absimle  11707  abstri  11727  abs2difabs  11731  bdtrilem  11862  bdtri  11863  xrmaxifle  11869  xrmaxadd  11884  xrbdtri  11899  climsqz  11958  climsqz2  11959  fsum3cvg2  12018  isumle  12119  expcnvap0  12126  expcnvre  12127  explecnv  12129  cvgratz  12156  efcllemp  12282  ege2le3  12295  eflegeo  12325  cos12dec  12392  fsumdvds  12466  phibnd  12852  pcdvdstr  12963  pcprmpw2  12969  pockthg  12993  2expltfac  13075  znrrg  14739  psmetres2  15127  xmetres2  15173  comet  15293  bdxmet  15295  cnmet  15324  ivthdec  15438  limcimolemlt  15458  tangtx  15632  logbgcd1irraplemap  15763  2lgslem1c  15892  cvgcmp2nlemabs  16747  trilpolemlt1  16756