Theorem 3brtr4d 4114

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

Syntax hints:   → wi 4   = wceq 1395   class class class wbr 4082

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-br 4083

This theorem is referenced by:  f1oiso2  5950  prarloclemarch2  7602  caucvgprprlemmu  7878  caucvgsrlembound  7977  mulap0  8797  lediv12a  9037  recp1lt1  9042  xleadd1a  10065  fldiv4p1lem1div2  10520  fldiv4lem1div2  10522  intfracq  10537  modqmulnn  10559  addmodlteq  10615  frecfzennn  10643  monoord2  10703  expgt1  10794  leexp2r  10810  leexp1a  10811  bernneq  10877  faclbnd  10958  faclbnd6  10961  facubnd  10962  hashunlem  11021  zfz1isolemiso  11056  sqrtgt0  11540  absrele  11589  absimle  11590  abstri  11610  abs2difabs  11614  bdtrilem  11745  bdtri  11746  xrmaxifle  11752  xrmaxadd  11767  xrbdtri  11782  climsqz  11841  climsqz2  11842  fsum3cvg2  11900  isumle  12001  expcnvap0  12008  expcnvre  12009  explecnv  12011  cvgratz  12038  efcllemp  12164  ege2le3  12177  eflegeo  12207  cos12dec  12274  fsumdvds  12348  phibnd  12734  pcdvdstr  12845  pcprmpw2  12851  pockthg  12875  2expltfac  12957  znrrg  14618  psmetres2  15001  xmetres2  15047  comet  15167  bdxmet  15169  cnmet  15198  ivthdec  15312  limcimolemlt  15332  tangtx  15506  logbgcd1irraplemap  15637  2lgslem1c  15763  cvgcmp2nlemabs  16359  trilpolemlt1  16368