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

Theorem syl6req 2089
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 2088 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2045 1  |-  ( ph  ->  C  =  A )
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