Theorem 3brtr4g 5129

Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.)

Hypotheses

Ref	Expression
3brtr4g.1	⊢ (𝜑 → 𝐴𝑅𝐵)
3brtr4g.2	⊢ 𝐶 = 𝐴
3brtr4g.3	⊢ 𝐷 = 𝐵

Assertion

Ref	Expression
3brtr4g	⊢ (𝜑 → 𝐶𝑅𝐷)

Proof of Theorem 3brtr4g

Step	Hyp	Ref	Expression
1		3brtr4g.1	. 2 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		3brtr4g.2	. . 3 ⊢ 𝐶 = 𝐴
3		3brtr4g.3	. . 3 ⊢ 𝐷 = 𝐵
4	2, 3	breq12i 5104	. 2 ⊢ (𝐶𝑅𝐷 ↔ 𝐴𝑅𝐵)
5	1, 4	sylibr 234	1 ⊢ (𝜑 → 𝐶𝑅𝐷)

Syntax hints:   → wi 4   = wceq 1541   class class class wbr 5095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096

This theorem is referenced by:  eqbrtrid  5130  enrefnn  8978  limensuci  9076  infensuc  9078  djuen  10071  djudom1  10084  rlimneg  15564  isumsup2  15763  crth  16699  4sqlem6  16865  gzrngunit  21380  matgsum  22362  ovolunlem1a  25434  ovolfiniun  25439  ioombl1lem1  25496  ioombl1lem4  25499  iblss  25743  itgle  25748  dvfsumlem3  25972  emcllem6  26948  gausslemma2dlem0f  27309  gausslemma2dlem0g  27310  pntpbnd1a  27533  ostth2lem4  27584  noinfbnd2lem1  27679  omsmon  34322  itg2gt0cn  37725  dalem-cly  39780  dalem10  39782  fourierdlem103  46321  fourierdlem104  46322