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

Theorem eqtr3 2059
 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 2042 . 2 (𝐵 = 𝐶𝐶 = 𝐵)
2 eqtr 2057 . 2 ((𝐴 = 𝐶𝐶 = 𝐵) → 𝐴 = 𝐵)
31, 2sylan2b 271 1 ((𝐴 = 𝐶𝐵 = 𝐶) → 𝐴 = 𝐵)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   = wceq 1243 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022 This theorem depends on definitions:  df-bi 110  df-cleq 2033 This theorem is referenced by:  eueq  2712  euind  2728  reuind  2744  preqsn  3546  eusv1  4184  funopg  4934  foco  5116  mpt2fun  5603  enq0tr  6532  lteupri  6715  elrealeu  6906  rereceu  6963  receuap  7650  xrltso  8717  xrlttri3  8718
 Copyright terms: Public domain W3C validator