Theorem 3brtr4g 4469

Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.)

Hypotheses

Ref	Expression
3brtr4g.1	|- ( ph -> A R B )
3brtr4g.2	|- C = A
3brtr4g.3	|- D = B

Assertion

Ref	Expression
3brtr4g	|- ( ph -> C R D )

Proof of Theorem 3brtr4g

Step	Hyp	Ref	Expression
1		3brtr4g.1	. 2 |- ( ph -> A R B )
2		3brtr4g.2	. . 3 |- C = A
3		3brtr4g.3	. . 3 |- D = B
4	2, 3	breq12i 4446	. 2 |- ( C R D <-> A R B )
5	1, 4	sylibr 212	1 |- ( ph -> C R D )

Syntax hints:   -> wi 4   = wceq 1383   class class class wbr 4437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438

This theorem is referenced by:  syl5eqbr  4470  limensuci  7695  infensuc  7697  rlimneg  13451  isumsup2  13640  crt  14290  4sqlem6  14443  gzrngunit  18462  matgsum  18917  ovolunlem1a  21885  ovolfiniun  21890  ioombl1lem1  21946  ioombl1lem4  21949  iblss  22189  itgle  22194  dvfsumlem3  22407  emcllem6  23308  pntpbnd1a  23748  ostth2lem4  23799  omsmon  28245  itg2gt0cn  30046  fourierdlem103  31946  fourierdlem104  31947  dalem-cly  35270  dalem10  35272