Theorem 3brtr4i 4437

Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.)

Hypotheses

Ref	Expression
3brtr4.1
3brtr4.2
3brtr4.3

Assertion

Ref	Expression
3brtr4i

Proof of Theorem 3brtr4i

Step	Hyp	Ref	Expression
1		3brtr4.2	. . 3
2		3brtr4.1	. . 3
3	1, 2	eqbrtri 4428	. 2
4		3brtr4.3	. 2
5	3, 4	breqtrri 4434	1

Syntax hints:  =wceq 1370   class class class wbr 4409

This theorem is referenced by:  1lt2nq  9279  0lt1sr  9399  declt  10915  decltc  10916  fzennn  11935  faclbnd4lem1  12226  fsumabs  13422  ovolfiniun  21383  log2ublem3  22743  log2ub  22744  emgt0  22800  bclbnd  23019  bposlem8  23030  nmblolbii  24668  normlem6  24986  norm-ii-i  25008  nmbdoplbi  25897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2809  df-v 3083  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3752  df-if 3906  df-sn 3994  df-pr 3996  df-op 4000  df-br 4410