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

Theorem sylan9eq 2193
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 2158 . 2  |-  ( ( A  =  B  /\  B  =  C )  ->  A  =  C )
41, 2, 3syl2an 287 1  |-  ( (
ph  /\  ps )  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    = wceq 1332
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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-cleq 2133
This theorem is referenced by:  sylan9req  2194  sylan9eqr  2195  difeq12  3193  uneq12  3229  ineq12  3276  ifeq12  3492  preq12  3609  prprc  3640  preq12b  3704  opeq12  3714  xpeq12  4565  nfimad  4897  coi2  5062  funimass1  5207  f1orescnv  5390  resdif  5396  oveq12  5790  cbvmpov  5858  ovmpog  5912  eqopi  6077  fmpoco  6120  nnaordex  6430  map0g  6589  xpcomco  6727  xpmapenlem  6750  phplem3  6755  phplem4  6756  sbthlemi5  6856  addcmpblnq  7198  ltrnqg  7251  enq0ref  7264  addcmpblnq0  7274  distrlem4prl  7415  distrlem4pru  7416  recexgt0sr  7604  axcnre  7712  cnegexlem2  7961  cnegexlem3  7962  recexap  8437  xaddpnf2  9659  xaddmnf2  9661  rexadd  9664  xaddnemnf  9669  xaddnepnf  9670  xposdif  9694  frec2uzrand  10208  seqeq3  10253  shftcan1  10637  remul2  10676  immul2  10683  ef0lem  11401  efieq1re  11512  dvdsnegb  11544  dvdscmul  11554  dvds2ln  11560  dvds2add  11561  dvds2sub  11562  gcdn0val  11684  rpmulgcd  11748  lcmval  11778  lcmn0val  11781  isopn3  12331  dvexp  12881  dvexp2  12882  subctctexmid  13367
  Copyright terms: Public domain W3C validator