Theorem 3brtr4d 4083

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

Syntax hints:   → wi 4   = wceq 1373   class class class wbr 4051

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-un 3174  df-sn 3644  df-pr 3645  df-op 3647  df-br 4052

This theorem is referenced by:  f1oiso2  5909  prarloclemarch2  7552  caucvgprprlemmu  7828  caucvgsrlembound  7927  mulap0  8747  lediv12a  8987  recp1lt1  8992  xleadd1a  10015  fldiv4p1lem1div2  10470  fldiv4lem1div2  10472  intfracq  10487  modqmulnn  10509  addmodlteq  10565  frecfzennn  10593  monoord2  10653  expgt1  10744  leexp2r  10760  leexp1a  10761  bernneq  10827  faclbnd  10908  faclbnd6  10911  facubnd  10912  hashunlem  10971  zfz1isolemiso  11006  sqrtgt0  11420  absrele  11469  absimle  11470  abstri  11490  abs2difabs  11494  bdtrilem  11625  bdtri  11626  xrmaxifle  11632  xrmaxadd  11647  xrbdtri  11662  climsqz  11721  climsqz2  11722  fsum3cvg2  11780  isumle  11881  expcnvap0  11888  expcnvre  11889  explecnv  11891  cvgratz  11918  efcllemp  12044  ege2le3  12057  eflegeo  12087  cos12dec  12154  fsumdvds  12228  phibnd  12614  pcdvdstr  12725  pcprmpw2  12731  pockthg  12755  2expltfac  12837  znrrg  14497  psmetres2  14880  xmetres2  14926  comet  15046  bdxmet  15048  cnmet  15077  ivthdec  15191  limcimolemlt  15211  tangtx  15385  logbgcd1irraplemap  15516  2lgslem1c  15642  cvgcmp2nlemabs  16112  trilpolemlt1  16121