Theorem 3brtr4d 4162

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402   class class class wbr 4130

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-br 4131

This theorem is used by:  f1oiso2  6033  prarloclemarch2  7787  caucvgprprlemmu  8063  caucvgsrlembound  8162  mulap0  8985  lediv12a  9227  recp1lt1  9232  xleadd1a  10286  fldiv4p1lem1div2  10755  fldiv4lem1div2  10757  intfracq  10772  modqmulnn  10794  addmodlteq  10850  frecfzennn  10878  monoord2  10938  expgt1  11029  leexp2r  11045  leexp1a  11046  bernneq  11113  faclbnd  11195  faclbnd6  11198  facubnd  11199  hashunlem  11260  zfz1isolemiso  11307  sqrtgt0  11816  absrele  11866  absimle  11867  abstri  11887  abs2difabs  11891  bdtrilem  12024  bdtri  12025  xrmaxifle  12031  xrmaxadd  12046  xrbdtri  12061  climsqz  12120  climsqz2  12121  fsum3cvg2  12180  isumle  12281  expcnvap0  12288  expcnvre  12289  explecnv  12291  cvgratz  12318  efcllemp  12444  ege2le3  12457  eflegeo  12487  cos12dec  12554  fsumdvds  12628  phibnd  13018  pcdvdstr  13129  pcprmpw2  13135  pockthg  13159  2expltfac  13242  znrrg  15086  psmetres2  15533  xmetres2  15579  comet  15699  bdxmet  15701  cnmet  15730  ivthdec  15844  limcimolemlt  15864  efap1p  15979  tangtx  16039  logbgcd1irraplemap  16179  birthdaylem3  16201  chtqwordi  16237  ppiqwordi  16242  ppiqub  16267  chtqleppi  16268  chtublem  16269  chtqub  16270  bcmono  16278  bclbnd  16281  bposlem1  16285  bposlem6  16290  bposlem9  16293  2lgslem1c  16388  cvgcmp2nlemabs  17260  trilpolemlt1  17270