Theorem 3brtr4g 5109

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

Syntax hints:   → wi 4   = wceq 1548   class class class wbr 5075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-br 5076

This theorem is referenced by:  eqbrtrid  5110  enrefnn  8987  limensuci  9085  infensuc  9087  djuen  10087  djudom1  10100  rlimneg  15604  isumsup2  15806  crth  16743  4sqlem6  16909  gzrngunit  21412  matgsum  22424  ovolunlem1a  25485  ovolfiniun  25490  ioombl1lem1  25547  ioombl1lem4  25550  iblss  25794  itgle  25799  dvfsumlem3  26017  emcllem6  26986  gausslemma2dlem0f  27346  gausslemma2dlem0g  27347  pntpbnd1a  27570  ostth2lem4  27621  noinfbnd2lem1  27716  omsmon  34494  itg2gt0cn  38057  dalem-cly  40178  dalem10  40180  fourierdlem103  46666  fourierdlem104  46667