Theorem breqtri 4070

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
breqtr.1	|- A R B
breqtr.2	|- B = C

Assertion

Ref	Expression
breqtri	|- A R C

Proof of Theorem breqtri

Step	Hyp	Ref	Expression
1		breqtr.1	. 2 |- A R B
2		breqtr.2	. . 3 |- B = C
3	2	breq2i 4053	. 2 |- ( A R B <-> A R C )
4	1, 3	mpbi 145	1 |- A R C

Syntax hints:   = wceq 1373   class class class wbr 4045

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-br 4046

This theorem is referenced by:  breqtrri  4072  3brtr3i  4074  le9lt10  9532  9lt10  9636  sqrt2gt1lt2  11393  trireciplem  11844  cos1bnd  12103  cos2bnd  12104  cos01gt0  12107  sin4lt0  12111  z4even  12260  dec2dvds  12767  coseq00topi  15340  sincos4thpi  15345  lgsdir2lem2  15539  lgsdir2lem3  15540  ex-fl  15698