MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3brtr4i Unicode version

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
StepHypRef Expression
1 3brtr4.2 . . 3
2 3brtr4.1 . . 3
31, 2eqbrtri 4428 . 2
4 3brtr4.3 . 2
53, 4breqtrri 4434 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator