Theorem 3brtr4g 5108

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

Syntax hints:   → wi 4   = wceq 1539   class class class wbr 5074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075

This theorem is referenced by:  eqbrtrid  5109  enrefnn  8837  enpr2d  8838  limensuci  8940  infensuc  8942  djuen  9925  djudom1  9938  rlimneg  15358  isumsup2  15558  crth  16479  4sqlem6  16644  gzrngunit  20664  matgsum  21586  ovolunlem1a  24660  ovolfiniun  24665  ioombl1lem1  24722  ioombl1lem4  24725  iblss  24969  itgle  24974  dvfsumlem3  25192  emcllem6  26150  gausslemma2dlem0f  26509  gausslemma2dlem0g  26510  pntpbnd1a  26733  ostth2lem4  26784  omsmon  32265  noinfbnd2lem1  33933  itg2gt0cn  35832  dalem-cly  37685  dalem10  37687  fourierdlem103  43750  fourierdlem104  43751