Theorem 3brtr4g 5104

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071

This theorem is referenced by:  eqbrtrid  5105  enrefnn  8791  enpr2d  8792  limensuci  8889  infensuc  8891  djuen  9856  djudom1  9869  rlimneg  15286  isumsup2  15486  crth  16407  4sqlem6  16572  gzrngunit  20576  matgsum  21494  ovolunlem1a  24565  ovolfiniun  24570  ioombl1lem1  24627  ioombl1lem4  24630  iblss  24874  itgle  24879  dvfsumlem3  25097  emcllem6  26055  gausslemma2dlem0f  26414  gausslemma2dlem0g  26415  pntpbnd1a  26638  ostth2lem4  26689  omsmon  32165  noinfbnd2lem1  33860  itg2gt0cn  35759  dalem-cly  37612  dalem10  37614  fourierdlem103  43640  fourierdlem104  43641