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

Theorem eqtr3 2197
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 2179 . 2 (𝐵 = 𝐶𝐶 = 𝐵)
2 eqtr 2195 . 2 ((𝐴 = 𝐶𝐶 = 𝐵) → 𝐴 = 𝐵)
31, 2sylan2b 287 1 ((𝐴 = 𝐶𝐵 = 𝐶) → 𝐴 = 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104   = wceq 1353
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-cleq 2170
This theorem is referenced by:  eueq  2908  euind  2924  reuind  2942  preqsn  3775  eusv1  4452  funopg  5250  funinsn  5265  foco  5448  mpofun  5976  enq0tr  7432  lteupri  7615  elrealeu  7827  rereceu  7887  receuap  8625  xrltso  9795  xrlttri3  9796  iseqf1olemab  10488  fsumparts  11477  odd2np1  11877  grpinveu  12910  exmidsbthrlem  14740
  Copyright terms: Public domain W3C validator