Theorem 3brtr4d 4053

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

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

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 2171

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-un 3148  df-sn 3616  df-pr 3617  df-op 3619  df-br 4022

This theorem is referenced by:  f1oiso2  5852  prarloclemarch2  7453  caucvgprprlemmu  7729  caucvgsrlembound  7828  mulap0  8646  lediv12a  8886  recp1lt1  8891  xleadd1a  9909  fldiv4p1lem1div2  10342  intfracq  10357  modqmulnn  10379  addmodlteq  10435  frecfzennn  10463  monoord2  10516  expgt1  10598  leexp2r  10614  leexp1a  10615  bernneq  10681  faclbnd  10762  faclbnd6  10765  facubnd  10766  hashunlem  10825  zfz1isolemiso  10860  sqrtgt0  11084  absrele  11133  absimle  11134  abstri  11154  abs2difabs  11158  bdtrilem  11288  bdtri  11289  xrmaxifle  11295  xrmaxadd  11310  xrbdtri  11325  climsqz  11384  climsqz2  11385  fsum3cvg2  11443  isumle  11544  expcnvap0  11551  expcnvre  11552  explecnv  11554  cvgratz  11581  efcllemp  11707  ege2le3  11720  eflegeo  11750  cos12dec  11816  phibnd  12260  pcdvdstr  12370  pcprmpw2  12376  pockthg  12400  psmetres2  14318  xmetres2  14364  comet  14484  bdxmet  14486  cnmet  14515  ivthdec  14607  limcimolemlt  14618  tangtx  14744  logbgcd1irraplemap  14872  cvgcmp2nlemabs  15268  trilpolemlt1  15277