Theorem 3brtr4d 4030

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

Syntax hints:   → wi 4   = wceq 1353   class class class wbr 3998

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-v 2737  df-un 3131  df-sn 3595  df-pr 3596  df-op 3598  df-br 3999

This theorem is referenced by:  f1oiso2  5818  prarloclemarch2  7393  caucvgprprlemmu  7669  caucvgsrlembound  7768  mulap0  8584  lediv12a  8824  recp1lt1  8829  xleadd1a  9844  fldiv4p1lem1div2  10275  intfracq  10290  modqmulnn  10312  addmodlteq  10368  frecfzennn  10396  monoord2  10447  expgt1  10528  leexp2r  10544  leexp1a  10545  bernneq  10610  faclbnd  10689  faclbnd6  10692  facubnd  10693  hashunlem  10752  zfz1isolemiso  10787  sqrtgt0  11011  absrele  11060  absimle  11061  abstri  11081  abs2difabs  11085  bdtrilem  11215  bdtri  11216  xrmaxifle  11222  xrmaxadd  11237  xrbdtri  11252  climsqz  11311  climsqz2  11312  fsum3cvg2  11370  isumle  11471  expcnvap0  11478  expcnvre  11479  explecnv  11481  cvgratz  11508  efcllemp  11634  ege2le3  11647  eflegeo  11677  cos12dec  11743  phibnd  12184  pcdvdstr  12293  pcprmpw2  12299  pockthg  12322  psmetres2  13413  xmetres2  13459  comet  13579  bdxmet  13581  cnmet  13610  ivthdec  13702  limcimolemlt  13713  tangtx  13839  logbgcd1irraplemap  13967  cvgcmp2nlemabs  14350  trilpolemlt1  14359