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  2080  xpcan  5434  xpcan2  5435  mapxpen  7673  sucdom2  7704  f1finf1o  7736  unfi  7776  inf3lem3  8036  dfac12r  8515  cfsuc  8626  fin23lem26  8694  iundom2g  8904  inar1  9142  rankcf  9144  ltsrpr  9443  supsrlem  9477  axpre-sup  9535  infmrcl  10511  nominpos  10764  ublbneg  11155  qbtwnre  11387  fsequb  12041  brfi1uzind  12485  rexanre  13128  rexuzre  13134  rexico  13135  caubnd  13140  rlim2lt  13269  rlim3  13270  lo1bddrp  13297  o1lo1  13309  climshftlem  13346  rlimcn2  13362  rlimo1  13388  lo1add  13398  lo1mul  13399  lo1le  13423  isercoll  13439  serf0  13452  cvgcmp  13579  dvds1lem  13845  dvds2lem  13846  isprm5  14101  vdwlem2  14348  vdwlem10  14356  vdwlem11  14357  lsmcv  17563  lmconst  19521  ptcnplem  19850  fclscmp  20259  tsmsresOLD  20373  tsmsres  20374  addcnlem  21096  lebnumlem3  21191  xlebnum  21193  lebnumii  21194  iscmet3lem2  21459  bcthlem4  21494  cniccbdd  21601  ovoliunlem2  21642  mbfi1flimlem  21857  ply1divex  22265  aalioulem3  22457  aalioulem5  22459  aalioulem6  22460  aaliou  22461  ulmshftlem  22511  ulmbdd  22520  tanarg  22725  cxploglim  23028  ftalem2  23068  ftalem7  23073  dchrisumlem3  23397  nvnencycllem  24305  ubthlem3  25314  spansncol  26012  riesz1  26510  erdsze2lem2  28138  dfrdg4  29027  onsuct0  29333  neibastop2  29633  incsequz  29695  caushft  29708  equivbnd  29740  cntotbnd  29746  expgrowth  30659  frgraogt3nreg  31839  vk15.4j  32252  sstrALT2  32590  bj-bary1  33628  4atexlemex4  34744
  Copyright terms: Public domain W3C validator