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  7786  caucvgprprlemmu  8062  caucvgsrlembound  8161  mulap0  8984  lediv12a  9226  recp1lt1  9231  xleadd1a  10285  fldiv4p1lem1div2  10753  fldiv4lem1div2  10755  intfracq  10770  modqmulnn  10792  addmodlteq  10848  frecfzennn  10876  monoord2  10936  expgt1  11027  leexp2r  11043  leexp1a  11044  bernneq  11111  faclbnd  11193  faclbnd6  11196  facubnd  11197  hashunlem  11258  zfz1isolemiso  11305  sqrtgt0  11814  absrele  11864  absimle  11865  abstri  11885  abs2difabs  11889  bdtrilem  12021  bdtri  12022  xrmaxifle  12028  xrmaxadd  12043  xrbdtri  12058  climsqz  12117  climsqz2  12118  fsum3cvg2  12177  isumle  12278  expcnvap0  12285  expcnvre  12286  explecnv  12288  cvgratz  12315  efcllemp  12441  ege2le3  12454  eflegeo  12484  cos12dec  12551  fsumdvds  12625  phibnd  13015  pcdvdstr  13126  pcprmpw2  13132  pockthg  13156  2expltfac  13239  znrrg  15044  psmetres2  15483  xmetres2  15529  comet  15649  bdxmet  15651  cnmet  15680  ivthdec  15794  limcimolemlt  15814  efap1p  15929  tangtx  15989  logbgcd1irraplemap  16124  birthdaylem3  16146  ppiqwordi  16174  ppiqub  16194  bcmono  16202  bclbnd  16205  bposlem1  16209  2lgslem1c  16307  cvgcmp2nlemabs  17179  trilpolemlt1  17188