Theorem 3brtr4g 5136

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

Syntax hints:   → wi 4   = wceq 1562   class class class wbr 5102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5103

This theorem is referenced by:  eqbrtrid  5137  enrefnn  9029  limensuci  9127  infensuc  9129  djuen  10128  djudom1  10141  rlimneg  15676  isumsup2  15878  crth  16815  4sqlem6  16981  gzrngunit  21487  matgsum  22499  ovolunlem1a  25560  ovolfiniun  25565  ioombl1lem1  25622  ioombl1lem4  25625  iblss  25869  itgle  25874  dvfsumlem3  26092  emcllem6  27067  gausslemma2dlem0f  27427  gausslemma2dlem0g  27428  pntpbnd1a  27651  ostth2lem4  27702  noinfbnd2lem1  27796  omsmon  34597  itg2gt0cn  38179  dalem-cly  40300  dalem10  40302  fourierdlem103  46788  fourierdlem104  46789