Theorem 3brtr4d 4162

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402   class class class wbr 4130

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-br 4131

This theorem is used by:  f1oiso2  6033  prarloclemarch2  7786  caucvgprprlemmu  8062  caucvgsrlembound  8161  mulap0  8982  lediv12a  9224  recp1lt1  9229  xleadd1a  10275  fldiv4p1lem1div2  10740  fldiv4lem1div2  10742  intfracq  10757  modqmulnn  10779  addmodlteq  10835  frecfzennn  10863  monoord2  10923  expgt1  11014  leexp2r  11030  leexp1a  11031  bernneq  11098  faclbnd  11179  faclbnd6  11182  facubnd  11183  hashunlem  11244  zfz1isolemiso  11291  sqrtgt0  11800  absrele  11849  absimle  11850  abstri  11870  abs2difabs  11874  bdtrilem  12005  bdtri  12006  xrmaxifle  12012  xrmaxadd  12027  xrbdtri  12042  climsqz  12101  climsqz2  12102  fsum3cvg2  12161  isumle  12262  expcnvap0  12269  expcnvre  12270  explecnv  12272  cvgratz  12299  efcllemp  12425  ege2le3  12438  eflegeo  12468  cos12dec  12535  fsumdvds  12609  phibnd  12995  pcdvdstr  13106  pcprmpw2  13112  pockthg  13136  2expltfac  13218  znrrg  14995  psmetres2  15434  xmetres2  15480  comet  15600  bdxmet  15602  cnmet  15631  ivthdec  15745  limcimolemlt  15765  tangtx  15939  logbgcd1irraplemap  16071  birthdaylem3  16089  2lgslem1c  16209  cvgcmp2nlemabs  17081  trilpolemlt1  17090