Theorem 3brtr4d 4075

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

Syntax hints:   → wi 4   = wceq 1372   class class class wbr 4043

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-un 3169  df-sn 3638  df-pr 3639  df-op 3641  df-br 4044

This theorem is referenced by:  f1oiso2  5886  prarloclemarch2  7514  caucvgprprlemmu  7790  caucvgsrlembound  7889  mulap0  8709  lediv12a  8949  recp1lt1  8954  xleadd1a  9977  fldiv4p1lem1div2  10429  fldiv4lem1div2  10431  intfracq  10446  modqmulnn  10468  addmodlteq  10524  frecfzennn  10552  monoord2  10612  expgt1  10703  leexp2r  10719  leexp1a  10720  bernneq  10786  faclbnd  10867  faclbnd6  10870  facubnd  10871  hashunlem  10930  zfz1isolemiso  10965  sqrtgt0  11264  absrele  11313  absimle  11314  abstri  11334  abs2difabs  11338  bdtrilem  11469  bdtri  11470  xrmaxifle  11476  xrmaxadd  11491  xrbdtri  11506  climsqz  11565  climsqz2  11566  fsum3cvg2  11624  isumle  11725  expcnvap0  11732  expcnvre  11733  explecnv  11735  cvgratz  11762  efcllemp  11888  ege2le3  11901  eflegeo  11931  cos12dec  11998  fsumdvds  12072  phibnd  12458  pcdvdstr  12569  pcprmpw2  12575  pockthg  12599  2expltfac  12681  znrrg  14340  psmetres2  14723  xmetres2  14769  comet  14889  bdxmet  14891  cnmet  14920  ivthdec  15034  limcimolemlt  15054  tangtx  15228  logbgcd1irraplemap  15359  2lgslem1c  15485  cvgcmp2nlemabs  15835  trilpolemlt1  15844