Theorem 3brtr4d 4062

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

Syntax hints:   → wi 4   = wceq 1364   class class class wbr 4030

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3158  df-sn 3625  df-pr 3626  df-op 3628  df-br 4031

This theorem is referenced by:  f1oiso2  5871  prarloclemarch2  7481  caucvgprprlemmu  7757  caucvgsrlembound  7856  mulap0  8675  lediv12a  8915  recp1lt1  8920  xleadd1a  9942  fldiv4p1lem1div2  10377  fldiv4lem1div2  10379  intfracq  10394  modqmulnn  10416  addmodlteq  10472  frecfzennn  10500  monoord2  10560  expgt1  10651  leexp2r  10667  leexp1a  10668  bernneq  10734  faclbnd  10815  faclbnd6  10818  facubnd  10819  hashunlem  10878  zfz1isolemiso  10913  sqrtgt0  11181  absrele  11230  absimle  11231  abstri  11251  abs2difabs  11255  bdtrilem  11385  bdtri  11386  xrmaxifle  11392  xrmaxadd  11407  xrbdtri  11422  climsqz  11481  climsqz2  11482  fsum3cvg2  11540  isumle  11641  expcnvap0  11648  expcnvre  11649  explecnv  11651  cvgratz  11678  efcllemp  11804  ege2le3  11817  eflegeo  11847  cos12dec  11914  phibnd  12358  pcdvdstr  12468  pcprmpw2  12474  pockthg  12498  znrrg  14159  psmetres2  14512  xmetres2  14558  comet  14678  bdxmet  14680  cnmet  14709  ivthdec  14823  limcimolemlt  14843  tangtx  15014  logbgcd1irraplemap  15142  2lgslem1c  15247  cvgcmp2nlemabs  15592  trilpolemlt1  15601