Theorem 3brtr4g 4426

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 4403	. 2 |- ( C R D <-> A R B )
5	1, 4	sylibr 212	1 |- ( ph -> C R D )

Syntax hints:   -> wi 4   = wceq 1405   class class class wbr 4394

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-br 4395

This theorem is referenced by:  syl5eqbr  4427  limensuci  7730  infensuc  7732  rlimneg  13616  isumsup2  13807  crt  14515  4sqlem6  14668  gzrngunit  18801  matgsum  19229  ovolunlem1a  22197  ovolfiniun  22202  ioombl1lem1  22258  ioombl1lem4  22261  iblss  22501  itgle  22506  dvfsumlem3  22719  emcllem6  23654  pntpbnd1a  24149  ostth2lem4  24200  omsmon  28732  itg2gt0cn  31423  dalem-cly  32668  dalem10  32670  fourierdlem103  37341  fourierdlem104  37342