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

Theorem syl6an 683
Description: A syllogism deduction combined with conjoining antecedents. (Contributed by Alan Sare, 28-Oct-2011.)
Hypotheses
Ref Expression
syl6an.1 (𝜑𝜓)
syl6an.2 (𝜑 → (𝜒𝜃))
syl6an.3 ((𝜓𝜃) → 𝜏)
Assertion
Ref Expression
syl6an (𝜑 → (𝜒𝜏))

Proof of Theorem syl6an
StepHypRef Expression
1 syl6an.1 . 2 (𝜑𝜓)
2 syl6an.2 . 2 (𝜑 → (𝜒𝜃))
3 syl6an.3 . . 3 ((𝜓𝜃) → 𝜏)
43ex 414 . 2 (𝜓 → (𝜃𝜏))
51, 2, 4sylsyld 61 1 (𝜑 → (𝜒𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  dfsb2  2492  xpcan  6129  xpcan2  6130  sucdom2OLD  9029  mapxpen  9090  sucdom2  9153  f1finf1oOLD  9219  unfiOLD  9260  inf3lem3  9571  dfac12r  10087  nnadju  10138  cfsuc  10198  fin23lem26  10266  iundom2g  10481  inar1  10716  rankcf  10718  ltsrpr  11018  supsrlem  11052  axpre-sup  11110  nominpos  12395  ublbneg  12863  qbtwnre  13124  fsequb  13886  fi1uzind  14402  brfi1indALT  14405  ccats1pfxeqrex  14609  rexanre  15237  rexuzre  15243  rexico  15244  caubnd  15249  rlim2lt  15385  rlim3  15386  lo1bddrp  15413  o1lo1  15425  climshftlem  15462  rlimcn3  15478  rlimo1  15505  lo1add  15515  lo1mul  15516  lo1le  15542  isercoll  15558  serf0  15571  cvgcmp  15706  dvds1lem  16155  dvds2lem  16156  mulmoddvds  16217  isprm5  16588  vdwlem2  16859  vdwlem10  16867  vdwlem11  16868  lsmcv  20618  lmconst  22628  ptcnplem  22988  fclscmp  23397  tsmsres  23511  addcnlem  24243  lebnumlem3  24342  xlebnum  24344  lebnumii  24345  iscmet3lem2  24672  bcthlem4  24707  cniccbdd  24841  ovoliunlem2  24883  mbfi1flimlem  25103  ply1divex  25517  aalioulem3  25710  aalioulem5  25712  aalioulem6  25713  aaliou  25714  ulmshftlem  25764  ulmbdd  25773  tanarg  25990  cxploglim  26343  ftalem2  26439  ftalem7  26444  dchrisumlem3  26855  frgrogt3nreg  29383  ubthlem3  29856  spansncol  30552  riesz1  31049  fineqvac  33755  erdsze2lem2  33855  dfrdg4  34582  neibastop2  34879  onsuct0  34959  bj-bary1  35829  topdifinffinlem  35864  finorwe  35899  poimirlem24  36148  incsequz  36253  caushft  36266  equivbnd  36295  cntotbnd  36301  4atexlemex4  38582  frege124d  42121  gneispace  42494  expgrowth  42703  vk15.4j  42898  sstrALT2  43205  iccpartdisj  45715  fppr2odd  46009
  Copyright terms: Public domain W3C validator