ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqtr3 GIF version

Theorem eqtr3 2073
Description: A transitive law for class equality. (Contributed by NM, 20-May-2005.)
Assertion
Ref Expression
eqtr3 ((𝐴 = 𝐶𝐵 = 𝐶) → 𝐴 = 𝐵)

Proof of Theorem eqtr3
StepHypRef Expression
1 eqcom 2056 . 2 (𝐵 = 𝐶𝐶 = 𝐵)
2 eqtr 2071 . 2 ((𝐴 = 𝐶𝐶 = 𝐵) → 𝐴 = 𝐵)
31, 2sylan2b 275 1 ((𝐴 = 𝐶𝐵 = 𝐶) → 𝐴 = 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101   = wceq 1257
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1350  ax-gen 1352  ax-4 1414  ax-17 1433  ax-ext 2036
This theorem depends on definitions:  df-bi 114  df-cleq 2047
This theorem is referenced by:  eueq  2732  euind  2748  reuind  2764  preqsn  3571  eusv1  4209  funopg  4959  foco  5141  mpt2fun  5628  enq0tr  6560  lteupri  6743  elrealeu  6934  rereceu  6991  receuap  7694  xrltso  8788  xrlttri3  8789  odd2np1  10147
  Copyright terms: Public domain W3C validator