Theorem 3brtr4g 5176

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

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

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-br 5143

This theorem is referenced by:  eqbrtrid  5177  enrefnn  9032  enpr2dOLD  9035  limensuci  9138  infensuc  9140  djuen  10148  djudom1  10161  rlimneg  15577  isumsup2  15776  crth  16695  4sqlem6  16860  gzrngunit  20947  matgsum  21870  ovolunlem1a  24944  ovolfiniun  24949  ioombl1lem1  25006  ioombl1lem4  25009  iblss  25253  itgle  25258  dvfsumlem3  25476  emcllem6  26434  gausslemma2dlem0f  26793  gausslemma2dlem0g  26794  pntpbnd1a  27017  ostth2lem4  27068  noinfbnd2lem1  27162  omsmon  33192  itg2gt0cn  36411  dalem-cly  38411  dalem10  38413  fourierdlem103  44762  fourierdlem104  44763