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

Theorem sylan9eq 2108
Description: An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
sylan9eq.1  |-  ( ph  ->  A  =  B )
sylan9eq.2  |-  ( ps 
->  B  =  C
)
Assertion
Ref Expression
sylan9eq  |-  ( (
ph  /\  ps )  ->  A  =  C )

Proof of Theorem sylan9eq
StepHypRef Expression
1 sylan9eq.1 . 2  |-  ( ph  ->  A  =  B )
2 sylan9eq.2 . 2  |-  ( ps 
->  B  =  C
)
3 eqtr 2073 . 2  |-  ( ( A  =  B  /\  B  =  C )  ->  A  =  C )
41, 2, 3syl2an 277 1  |-  ( (
ph  /\  ps )  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    = 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:  sylan9req  2109  sylan9eqr  2110  difeq12  3085  uneq12  3120  ineq12  3161  ifeq12  3372  preq12  3477  prprc  3508  preq12b  3569  opeq12  3579  xpeq12  4392  nfimad  4705  coi2  4865  funimass1  5004  f1orescnv  5170  resdif  5176  oveq12  5549  cbvmpt2v  5612  ovmpt2g  5663  eqopi  5826  fmpt2co  5865  nnaordex  6131  xpcomco  6331  phplem3  6348  phplem4  6349  addcmpblnq  6523  ltrnqg  6576  enq0ref  6589  addcmpblnq0  6599  distrlem4prl  6740  distrlem4pru  6741  recexgt0sr  6916  axcnre  7013  cnegexlem2  7250  cnegexlem3  7251  recexap  7708  frec2uzzd  9350  frec2uzrand  9355  iseqeq3  9380  shftcan1  9663  remul2  9701  immul2  9708  dvdsnegb  10125  dvdscmul  10134  dvds2ln  10140  dvds2add  10141  dvds2sub  10142
  Copyright terms: Public domain W3C validator