Theorem 3brtr4d 4115

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

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

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 4084

This theorem is referenced by:  f1oiso2  5957  prarloclemarch2  7617  caucvgprprlemmu  7893  caucvgsrlembound  7992  mulap0  8812  lediv12a  9052  recp1lt1  9057  xleadd1a  10081  fldiv4p1lem1div2  10537  fldiv4lem1div2  10539  intfracq  10554  modqmulnn  10576  addmodlteq  10632  frecfzennn  10660  monoord2  10720  expgt1  10811  leexp2r  10827  leexp1a  10828  bernneq  10894  faclbnd  10975  faclbnd6  10978  facubnd  10979  hashunlem  11038  zfz1isolemiso  11074  sqrtgt0  11560  absrele  11609  absimle  11610  abstri  11630  abs2difabs  11634  bdtrilem  11765  bdtri  11766  xrmaxifle  11772  xrmaxadd  11787  xrbdtri  11802  climsqz  11861  climsqz2  11862  fsum3cvg2  11920  isumle  12021  expcnvap0  12028  expcnvre  12029  explecnv  12031  cvgratz  12058  efcllemp  12184  ege2le3  12197  eflegeo  12227  cos12dec  12294  fsumdvds  12368  phibnd  12754  pcdvdstr  12865  pcprmpw2  12871  pockthg  12895  2expltfac  12977  znrrg  14639  psmetres2  15022  xmetres2  15068  comet  15188  bdxmet  15190  cnmet  15219  ivthdec  15333  limcimolemlt  15353  tangtx  15527  logbgcd1irraplemap  15658  2lgslem1c  15784  cvgcmp2nlemabs  16460  trilpolemlt1  16469