Theorem 3brtr4d 4008

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

Syntax hints:   → wi 4   = wceq 1342   class class class wbr 3976

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 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-v 2723  df-un 3115  df-sn 3576  df-pr 3577  df-op 3579  df-br 3977

This theorem is referenced by:  f1oiso2  5789  prarloclemarch2  7351  caucvgprprlemmu  7627  caucvgsrlembound  7726  mulap0  8542  lediv12a  8780  recp1lt1  8785  xleadd1a  9800  fldiv4p1lem1div2  10230  intfracq  10245  modqmulnn  10267  addmodlteq  10323  frecfzennn  10351  monoord2  10402  expgt1  10483  leexp2r  10499  leexp1a  10500  bernneq  10564  faclbnd  10643  faclbnd6  10646  facubnd  10647  hashunlem  10706  zfz1isolemiso  10738  sqrtgt0  10962  absrele  11011  absimle  11012  abstri  11032  abs2difabs  11036  bdtrilem  11166  bdtri  11167  xrmaxifle  11173  xrmaxadd  11188  xrbdtri  11203  climsqz  11262  climsqz2  11263  fsum3cvg2  11321  isumle  11422  expcnvap0  11429  expcnvre  11430  explecnv  11432  cvgratz  11459  efcllemp  11585  ege2le3  11598  eflegeo  11628  cos12dec  11694  phibnd  12126  pcdvdstr  12235  pcprmpw2  12241  psmetres2  12874  xmetres2  12920  comet  13040  bdxmet  13042  cnmet  13071  ivthdec  13163  limcimolemlt  13174  tangtx  13300  logbgcd1irraplemap  13428  cvgcmp2nlemabs  13745  trilpolemlt1  13754