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  2098  xpcan  5429  xpcan2  5430  mapxpen  7681  sucdom2  7712  f1finf1o  7744  unfi  7785  inf3lem3  8045  dfac12r  8524  cfsuc  8635  fin23lem26  8703  iundom2g  8913  inar1  9151  rankcf  9153  ltsrpr  9452  supsrlem  9486  axpre-sup  9544  infmrcl  10523  nominpos  10776  ublbneg  11170  qbtwnre  11402  fsequb  12059  brfi1uzind  12506  rexanre  13153  rexuzre  13159  rexico  13160  caubnd  13165  rlim2lt  13294  rlim3  13295  lo1bddrp  13322  o1lo1  13334  climshftlem  13371  rlimcn2  13387  rlimo1  13413  lo1add  13423  lo1mul  13424  lo1le  13448  isercoll  13464  serf0  13477  cvgcmp  13604  dvds1lem  13867  dvds2lem  13868  isprm5  14125  vdwlem2  14372  vdwlem10  14380  vdwlem11  14381  lsmcv  17655  lmconst  19628  ptcnplem  19988  fclscmp  20397  tsmsresOLD  20511  tsmsres  20512  addcnlem  21234  lebnumlem3  21329  xlebnum  21331  lebnumii  21332  iscmet3lem2  21597  bcthlem4  21632  cniccbdd  21739  ovoliunlem2  21780  mbfi1flimlem  21995  ply1divex  22403  aalioulem3  22595  aalioulem5  22597  aalioulem6  22598  aaliou  22599  ulmshftlem  22649  ulmbdd  22658  tanarg  22869  cxploglim  23172  ftalem2  23212  ftalem7  23217  dchrisumlem3  23541  nvnencycllem  24508  frgraogt3nreg  24985  ubthlem3  25653  spansncol  26351  riesz1  26849  erdsze2lem2  28514  dfrdg4  29568  onsuct0  29874  neibastop2  30147  incsequz  30209  caushft  30222  equivbnd  30254  cntotbnd  30260  expgrowth  31209  vk15.4j  33006  sstrALT2  33343  bj-bary1  34383  4atexlemex4  35499
  Copyright terms: Public domain W3C validator