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

Theorem syl6req 2103
Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
Hypotheses
Ref Expression
syl6req.1 (𝜑𝐴 = 𝐵)
syl6req.2 𝐵 = 𝐶
Assertion
Ref Expression
syl6req (𝜑𝐶 = 𝐴)

Proof of Theorem syl6req
StepHypRef Expression
1 syl6req.1 . . 3 (𝜑𝐴 = 𝐵)
2 syl6req.2 . . 3 𝐵 = 𝐶
31, 2syl6eq 2102 . 2 (𝜑𝐴 = 𝐶)
43eqcomd 2059 1 (𝜑𝐶 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1257
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1350  ax-gen 1352  ax-4 1414  ax-17 1433  ax-ext 2036
This theorem depends on definitions:  df-bi 114  df-cleq 2047
This theorem is referenced by:  syl6reqr  2105  elxp4  4833  elxp5  4834  fo1stresm  5813  fo2ndresm  5814  eloprabi  5847  fo2ndf  5873  xpsnen  6323  xpassen  6332  ac6sfi  6380  ine0  7433  nn0n0n1ge2  8339  fzval2  8949  fseq1p1m1  9028  odd2np1  10147
  Copyright terms: Public domain W3C validator