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

Theorem eqtr3 2101
 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 2084 . 2 (𝐵 = 𝐶𝐶 = 𝐵)
2 eqtr 2099 . 2 ((𝐴 = 𝐶𝐶 = 𝐵) → 𝐴 = 𝐵)
31, 2sylan2b 281 1 ((𝐴 = 𝐶𝐵 = 𝐶) → 𝐴 = 𝐵)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 102   = wceq 1285 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064 This theorem depends on definitions:  df-bi 115  df-cleq 2075 This theorem is referenced by:  eueq  2764  euind  2780  reuind  2796  preqsn  3575  eusv1  4210  funopg  4964  funinsn  4979  foco  5147  mpt2fun  5634  enq0tr  6686  lteupri  6869  elrealeu  7060  rereceu  7117  receuap  7826  xrltso  8947  xrlttri3  8948  odd2np1  10417
 Copyright terms: Public domain W3C validator