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  2071  xpcan  5375  xpcan2  5376  mapxpen  7580  sucdom2  7611  f1finf1o  7643  unfi  7683  inf3lem3  7940  dfac12r  8419  cfsuc  8530  fin23lem26  8598  iundom2g  8808  inar1  9046  rankcf  9048  ltsrpr  9348  supsrlem  9382  axpre-sup  9440  infmrcl  10413  nominpos  10665  ublbneg  11043  qbtwnre  11273  fsequb  11907  brfi1uzind  12330  rexanre  12945  rexuzre  12951  rexico  12952  caubnd  12957  rlim2lt  13086  rlim3  13087  lo1bddrp  13114  o1lo1  13126  climshftlem  13163  rlimcn2  13179  rlimo1  13205  lo1add  13215  lo1mul  13216  lo1le  13240  isercoll  13256  serf0  13269  cvgcmp  13390  dvds1lem  13655  dvds2lem  13656  isprm5  13909  vdwlem2  14154  vdwlem10  14162  vdwlem11  14163  lsmcv  17337  lmconst  18990  ptcnplem  19319  fclscmp  19728  tsmsresOLD  19842  tsmsres  19843  addcnlem  20565  lebnumlem3  20660  xlebnum  20662  lebnumii  20663  iscmet3lem2  20928  bcthlem4  20963  cniccbdd  21070  ovoliunlem2  21111  mbfi1flimlem  21326  ply1divex  21734  aalioulem3  21926  aalioulem5  21928  aalioulem6  21929  aaliou  21930  ulmshftlem  21980  ulmbdd  21989  tanarg  22194  cxploglim  22497  ftalem2  22537  ftalem7  22542  dchrisumlem3  22866  nvnencycllem  23674  ubthlem3  24418  spansncol  25116  riesz1  25614  erdsze2lem2  27229  dfrdg4  28118  onsuct0  28424  neibastop2  28723  incsequz  28785  caushft  28798  equivbnd  28830  cntotbnd  28836  expgrowth  29750  frgraogt3nreg  30854  vk15.4j  31536  sstrALT2  31874  bj-bary1  32910  4atexlemex4  34026
  Copyright terms: Public domain W3C validator