Theorem 3brtr4g 5133

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

Syntax hints:   → wi 4   = wceq 1542   class class class wbr 5099

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100

This theorem is referenced by:  eqbrtrid  5134  enrefnn  8987  limensuci  9085  infensuc  9087  djuen  10084  djudom1  10097  rlimneg  15574  isumsup2  15773  crth  16709  4sqlem6  16875  gzrngunit  21392  matgsum  22385  ovolunlem1a  25457  ovolfiniun  25462  ioombl1lem1  25519  ioombl1lem4  25522  iblss  25766  itgle  25771  dvfsumlem3  25995  emcllem6  26971  gausslemma2dlem0f  27332  gausslemma2dlem0g  27333  pntpbnd1a  27556  ostth2lem4  27607  noinfbnd2lem1  27702  omsmon  34457  itg2gt0cn  37878  dalem-cly  39999  dalem10  40001  fourierdlem103  46520  fourierdlem104  46521