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

Theorem syl6req 2105
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 2104 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2061 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1259
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 1352  ax-gen 1354  ax-4 1416  ax-17 1435  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049
This theorem is referenced by:  syl6reqr  2107  elxp4  4836  elxp5  4837  fo1stresm  5816  fo2ndresm  5817  eloprabi  5850  fo2ndf  5876  xpsnen  6326  xpassen  6335  ac6sfi  6383  ine0  7463  nn0n0n1ge2  8369  fzval2  8979  fseq1p1m1  9058  odd2np1  10184
  Copyright terms: Public domain W3C validator