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

Theorem syl6an 543
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 541 . 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 367
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 369
This theorem is referenced by:  dfsb2  2116  xpcan  5428  xpcan2  5429  mapxpen  7676  sucdom2  7707  f1finf1o  7739  unfi  7779  inf3lem3  8038  dfac12r  8517  cfsuc  8628  fin23lem26  8696  iundom2g  8906  inar1  9142  rankcf  9144  ltsrpr  9443  supsrlem  9477  axpre-sup  9535  infmrcl  10517  nominpos  10771  ublbneg  11167  qbtwnre  11401  fsequb  12070  brfi1uzind  12519  rexanre  13264  rexuzre  13270  rexico  13271  caubnd  13276  rlim2lt  13405  rlim3  13406  lo1bddrp  13433  o1lo1  13445  climshftlem  13482  rlimcn2  13498  rlimo1  13524  lo1add  13534  lo1mul  13535  lo1le  13559  isercoll  13575  serf0  13588  cvgcmp  13715  dvds1lem  14082  dvds2lem  14083  isprm5  14340  vdwlem2  14587  vdwlem10  14595  vdwlem11  14596  lsmcv  17985  lmconst  19932  ptcnplem  20291  fclscmp  20700  tsmsresOLD  20814  tsmsres  20815  addcnlem  21537  lebnumlem3  21632  xlebnum  21634  lebnumii  21635  iscmet3lem2  21900  bcthlem4  21935  cniccbdd  22042  ovoliunlem2  22083  mbfi1flimlem  22298  ply1divex  22706  aalioulem3  22899  aalioulem5  22901  aalioulem6  22902  aaliou  22903  ulmshftlem  22953  ulmbdd  22962  tanarg  23175  cxploglim  23508  ftalem2  23548  ftalem7  23553  dchrisumlem3  23877  nvnencycllem  24848  frgraogt3nreg  25325  ubthlem3  25989  spansncol  26687  riesz1  27185  erdsze2lem2  28915  dfrdg4  29831  onsuct0  30137  neibastop2  30422  incsequz  30484  caushft  30497  equivbnd  30529  cntotbnd  30535  expgrowth  31484  ccats1pfxeqrex  32669  vk15.4j  33704  sstrALT2  34054  bj-bary1  35097  4atexlemex4  36213
  Copyright terms: Public domain W3C validator