Theorem 3brtr4d 4021

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

Syntax hints:   → wi 4   = wceq 1348   class class class wbr 3989

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-sn 3589  df-pr 3590  df-op 3592  df-br 3990

This theorem is referenced by:  f1oiso2  5806  prarloclemarch2  7381  caucvgprprlemmu  7657  caucvgsrlembound  7756  mulap0  8572  lediv12a  8810  recp1lt1  8815  xleadd1a  9830  fldiv4p1lem1div2  10261  intfracq  10276  modqmulnn  10298  addmodlteq  10354  frecfzennn  10382  monoord2  10433  expgt1  10514  leexp2r  10530  leexp1a  10531  bernneq  10596  faclbnd  10675  faclbnd6  10678  facubnd  10679  hashunlem  10739  zfz1isolemiso  10774  sqrtgt0  10998  absrele  11047  absimle  11048  abstri  11068  abs2difabs  11072  bdtrilem  11202  bdtri  11203  xrmaxifle  11209  xrmaxadd  11224  xrbdtri  11239  climsqz  11298  climsqz2  11299  fsum3cvg2  11357  isumle  11458  expcnvap0  11465  expcnvre  11466  explecnv  11468  cvgratz  11495  efcllemp  11621  ege2le3  11634  eflegeo  11664  cos12dec  11730  phibnd  12171  pcdvdstr  12280  pcprmpw2  12286  pockthg  12309  psmetres2  13127  xmetres2  13173  comet  13293  bdxmet  13295  cnmet  13324  ivthdec  13416  limcimolemlt  13427  tangtx  13553  logbgcd1irraplemap  13681  cvgcmp2nlemabs  14064  trilpolemlt1  14073