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

Theorem eqtr3 2137
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 2119 . 2 (𝐵 = 𝐶𝐶 = 𝐵)
2 eqtr 2135 . 2 ((𝐴 = 𝐶𝐶 = 𝐵) → 𝐴 = 𝐵)
31, 2sylan2b 285 1 ((𝐴 = 𝐶𝐵 = 𝐶) → 𝐴 = 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103   = wceq 1316
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 1408  ax-gen 1410  ax-4 1472  ax-17 1491  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110
This theorem is referenced by:  eueq  2828  euind  2844  reuind  2862  preqsn  3672  eusv1  4343  funopg  5127  funinsn  5142  foco  5325  mpofun  5841  enq0tr  7210  lteupri  7393  elrealeu  7605  rereceu  7665  receuap  8398  xrltso  9550  xrlttri3  9551  iseqf1olemab  10230  fsumparts  11207  odd2np1  11497  exmidsbthrlem  13144
  Copyright terms: Public domain W3C validator