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

Theorem eqtr3 2160
 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 2142 . 2 (𝐵 = 𝐶𝐶 = 𝐵)
2 eqtr 2158 . 2 ((𝐴 = 𝐶𝐶 = 𝐵) → 𝐴 = 𝐵)
31, 2sylan2b 285 1 ((𝐴 = 𝐶𝐵 = 𝐶) → 𝐴 = 𝐵)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   = wceq 1332 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122 This theorem depends on definitions:  df-bi 116  df-cleq 2133 This theorem is referenced by:  eueq  2860  euind  2876  reuind  2894  preqsn  3711  eusv1  4382  funopg  5166  funinsn  5181  foco  5364  mpofun  5882  enq0tr  7286  lteupri  7469  elrealeu  7681  rereceu  7741  receuap  8474  xrltso  9632  xrlttri3  9633  iseqf1olemab  10313  fsumparts  11291  odd2np1  11626  exmidsbthrlem  13411
 Copyright terms: Public domain W3C validator