MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl6an Structured version   Unicode version

Theorem syl6an 545
Description: A syllogism deduction combined with conjoining antecedents. (Contributed by Alan Sare, 28-Oct-2011.)
Hypotheses
Ref Expression
syl6an.1  |-  ( ph  ->  ps )
syl6an.2  |-  ( ph  ->  ( ch  ->  th )
)
syl6an.3  |-  ( ( ps  /\  th )  ->  ta )
Assertion
Ref Expression
syl6an  |-  ( ph  ->  ( ch  ->  ta ) )

Proof of Theorem syl6an
StepHypRef Expression
1 syl6an.2 . . 3  |-  ( ph  ->  ( ch  ->  th )
)
2 syl6an.1 . . 3  |-  ( ph  ->  ps )
31, 2jctild 543 . 2  |-  ( ph  ->  ( ch  ->  ( ps  /\  th ) ) )
4 syl6an.3 . 2  |-  ( ( ps  /\  th )  ->  ta )
53, 4syl6 33 1  |-  ( ph  ->  ( ch  ->  ta ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  dfsb2  2064  xpcan  5269  xpcan2  5270  mapxpen  7469  sucdom2  7499  f1finf1o  7531  unfi  7571  inf3lem3  7828  dfac12r  8307  cfsuc  8418  fin23lem26  8486  iundom2g  8696  inar1  8934  rankcf  8936  ltsrpr  9236  supsrlem  9270  axpre-sup  9328  infmrcl  10301  nominpos  10553  ublbneg  10931  qbtwnre  11161  fsequb  11789  brfi1uzind  12211  rexanre  12826  rexuzre  12832  rexico  12833  caubnd  12838  rlim2lt  12967  rlim3  12968  lo1bddrp  12995  o1lo1  13007  climshftlem  13044  rlimcn2  13060  rlimo1  13086  lo1add  13096  lo1mul  13097  lo1le  13121  isercoll  13137  serf0  13150  cvgcmp  13271  dvds1lem  13536  dvds2lem  13537  isprm5  13790  vdwlem2  14035  vdwlem10  14043  vdwlem11  14044  lsmcv  17199  lmconst  18840  ptcnplem  19169  fclscmp  19578  tsmsresOLD  19692  tsmsres  19693  addcnlem  20415  lebnumlem3  20510  xlebnum  20512  lebnumii  20513  iscmet3lem2  20778  bcthlem4  20813  cniccbdd  20920  ovoliunlem2  20961  mbfi1flimlem  21175  ply1divex  21583  aalioulem3  21775  aalioulem5  21777  aalioulem6  21778  aaliou  21779  ulmshftlem  21829  ulmbdd  21838  tanarg  22043  cxploglim  22346  ftalem2  22386  ftalem7  22391  dchrisumlem3  22715  nvnencycllem  23480  ubthlem3  24224  spansncol  24922  riesz1  25420  erdsze2lem2  27044  dfrdg4  27932  onsuct0  28239  neibastop2  28535  incsequz  28597  caushft  28610  equivbnd  28642  cntotbnd  28648  expgrowth  29562  frgraogt3nreg  30666  vk15.4j  31120  sstrALT2  31458  bj-bary1  32443  4atexlemex4  33557
  Copyright terms: Public domain W3C validator