Theorem 3brtr4d 4061

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

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

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 3157  df-sn 3624  df-pr 3625  df-op 3627  df-br 4030

This theorem is referenced by:  f1oiso2  5870  prarloclemarch2  7479  caucvgprprlemmu  7755  caucvgsrlembound  7854  mulap0  8673  lediv12a  8913  recp1lt1  8918  xleadd1a  9939  fldiv4p1lem1div2  10374  fldiv4lem1div2  10376  intfracq  10391  modqmulnn  10413  addmodlteq  10469  frecfzennn  10497  monoord2  10557  expgt1  10648  leexp2r  10664  leexp1a  10665  bernneq  10731  faclbnd  10812  faclbnd6  10815  facubnd  10816  hashunlem  10875  zfz1isolemiso  10910  sqrtgt0  11178  absrele  11227  absimle  11228  abstri  11248  abs2difabs  11252  bdtrilem  11382  bdtri  11383  xrmaxifle  11389  xrmaxadd  11404  xrbdtri  11419  climsqz  11478  climsqz2  11479  fsum3cvg2  11537  isumle  11638  expcnvap0  11645  expcnvre  11646  explecnv  11648  cvgratz  11675  efcllemp  11801  ege2le3  11814  eflegeo  11844  cos12dec  11911  phibnd  12355  pcdvdstr  12465  pcprmpw2  12471  pockthg  12495  znrrg  14148  psmetres2  14501  xmetres2  14547  comet  14667  bdxmet  14669  cnmet  14698  ivthdec  14798  limcimolemlt  14818  tangtx  14973  logbgcd1irraplemap  15101  cvgcmp2nlemabs  15522  trilpolemlt1  15531