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

Theorem syl6an 547
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 545 . 2  |-  ( ph  ->  ( ch  ->  ( ps  /\  th ) ) )
4 syl6an.3 . 2  |-  ( ( ps  /\  th )  ->  ta )
53, 4syl6 34 1  |-  ( ph  ->  ( ch  ->  ta ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  dfsb2  2167  xpcan  5289  xpcan2  5290  mapxpen  7741  sucdom2  7771  f1finf1o  7801  unfi  7841  inf3lem3  8138  dfac12r  8577  cfsuc  8688  fin23lem26  8756  iundom2g  8966  inar1  9201  rankcf  9203  ltsrpr  9502  supsrlem  9536  axpre-sup  9594  infmrclOLD  10594  nominpos  10850  ublbneg  11249  qbtwnre  11493  fsequb  12188  brfi1uzind  12647  rexanre  13398  rexuzre  13404  rexico  13405  caubnd  13410  rlim2lt  13549  rlim3  13550  lo1bddrp  13577  o1lo1  13589  climshftlem  13626  rlimcn2  13642  rlimo1  13668  lo1add  13678  lo1mul  13679  lo1le  13703  isercoll  13719  serf0  13735  cvgcmp  13864  dvds1lem  14302  dvds2lem  14303  isprm5  14639  vdwlem2  14920  vdwlem10  14928  vdwlem11  14929  lsmcv  18352  lmconst  20264  ptcnplem  20623  fclscmp  21032  tsmsres  21145  addcnlem  21883  lebnumlem3  21978  lebnumlem3OLD  21981  xlebnum  21983  lebnumii  21984  iscmet3lem2  22249  bcthlem4  22282  cniccbdd  22399  ovoliunlem2  22443  mbfi1flimlem  22667  ply1divex  23074  aalioulem3  23277  aalioulem5  23279  aalioulem6  23280  aaliou  23281  ulmshftlem  23331  ulmbdd  23340  tanarg  23555  cxploglim  23890  ftalem2  23985  ftalem7  23992  dchrisumlem3  24316  nvnencycllem  25357  frgraogt3nreg  25834  ubthlem3  26500  spansncol  27207  riesz1  27704  erdsze2lem2  29923  dfrdg4  30711  neibastop2  31010  onsuct0  31094  bj-bary1  31669  topdifinffinlem  31691  poimirlem24  31878  incsequz  31991  caushft  32004  equivbnd  32036  cntotbnd  32042  4atexlemex4  33557  frege124d  36213  expgrowth  36542  vk15.4j  36743  sstrALT2  37092  iccpartdisj  38463  ccats1pfxeqrex  38675
  Copyright terms: Public domain W3C validator