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

Theorem syl6req 2187
Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
Hypotheses
Ref Expression
syl6req.1  |-  ( ph  ->  A  =  B )
syl6req.2  |-  B  =  C
Assertion
Ref Expression
syl6req  |-  ( ph  ->  C  =  A )

Proof of Theorem syl6req
StepHypRef Expression
1 syl6req.1 . . 3  |-  ( ph  ->  A  =  B )
2 syl6req.2 . . 3  |-  B  =  C
31, 2syl6eq 2186 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2143 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1331
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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2119
This theorem depends on definitions:  df-bi 116  df-cleq 2130
This theorem is referenced by:  syl6reqr  2189  elxp4  5021  elxp5  5022  fo1stresm  6052  fo2ndresm  6053  eloprabi  6087  fo2ndf  6117  xpsnen  6708  xpassen  6717  ac6sfi  6785  undifdc  6805  ine0  8149  nn0n0n1ge2  9114  fzval2  9786  fseq1p1m1  9867  fsum2dlemstep  11196  modfsummodlemstep  11219  ef4p  11389  sin01bnd  11453  odd2np1  11559  sqpweven  11842  2sqpwodd  11843  psmetdmdm  12482  xmetdmdm  12514  dveflem  12844  abssinper  12916
  Copyright terms: Public domain W3C validator