Theorem 3brtr4g 5147

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

Syntax hints:   → wi 4   = wceq 1567   class class class wbr 5111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3423  df-v 3463  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4491  df-sn 4593  df-pr 4595  df-op 4599  df-br 5112

This theorem is referenced by:  eqbrtrid  5148  enrefnn  9043  limensuci  9141  infensuc  9143  djuen  10153  djudom1  10166  rlimneg  15698  isumsup2  15900  crth  16837  4sqlem6  17003  gzrngunit  21552  matgsum  22563  ovolunlem1a  25624  ovolfiniun  25629  ioombl1lem1  25686  ioombl1lem4  25689  iblss  25933  itgle  25938  dvfsumlem3  26156  emcllem6  27131  gausslemma2dlem0f  27491  gausslemma2dlem0g  27492  pntpbnd1a  27715  ostth2lem4  27766  noinfbnd2lem1  27860  omsmon  34633  itg2gt0cn  38249  dalem-cly  40370  dalem10  40372  fourierdlem103  46850  fourierdlem104  46851