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

Theorem syl6req 2167
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 2166 . 2 (𝜑𝐴 = 𝐶)
43eqcomd 2123 1 (𝜑𝐶 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = 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:  syl6reqr  2169  elxp4  4996  elxp5  4997  fo1stresm  6027  fo2ndresm  6028  eloprabi  6062  fo2ndf  6092  xpsnen  6683  xpassen  6692  ac6sfi  6760  undifdc  6780  ine0  8124  nn0n0n1ge2  9089  fzval2  9761  fseq1p1m1  9842  fsum2dlemstep  11171  modfsummodlemstep  11194  ef4p  11327  sin01bnd  11391  odd2np1  11497  sqpweven  11780  2sqpwodd  11781  psmetdmdm  12420  xmetdmdm  12452  dveflem  12782  abssinper  12854
  Copyright terms: Public domain W3C validator