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

Theorem syl6req 2089
 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 2088 . 2 (𝜑𝐴 = 𝐶)
43eqcomd 2045 1 (𝜑𝐶 = 𝐴)
 Colors of variables: wff set class Syntax hints:   → wi 4   = 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:  syl6reqr  2091  elxp4  4808  elxp5  4809  fo1stresm  5788  fo2ndresm  5789  eloprabi  5822  fo2ndf  5848  xpsnen  6295  xpassen  6304  ac6sfi  6352  ine0  7391  nn0n0n1ge2  8311  fzval2  8877  fseq1p1m1  8956
 Copyright terms: Public domain W3C validator