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

Theorem syl6an 663
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.2 . . 3 (𝜑 → (𝜒𝜃))
2 syl6an.1 . . 3 (𝜑𝜓)
31, 2jctild 515 . 2 (𝜑 → (𝜒 → (𝜓𝜃)))
4 syl6an.3 . 2 ((𝜓𝜃) → 𝜏)
53, 4syl6 35 1 (𝜑 → (𝜒𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 197  df-an 383
This theorem is referenced by:  dfsb2  2520  xpcan  5710  xpcan2  5711  mapxpen  8285  sucdom2  8315  f1finf1o  8346  unfi  8386  inf3lem3  8694  dfac12r  9173  cfsuc  9284  fin23lem26  9352  iundom2g  9567  inar1  9802  rankcf  9804  ltsrpr  10103  supsrlem  10137  axpre-sup  10195  nominpos  11475  ublbneg  11980  qbtwnre  12234  fsequb  12981  fi1uzind  13480  brfi1indALT  13483  rexanre  14293  rexuzre  14299  rexico  14300  caubnd  14305  rlim2lt  14435  rlim3  14436  lo1bddrp  14463  o1lo1  14475  climshftlem  14512  rlimcn2  14528  rlimo1  14554  lo1add  14564  lo1mul  14565  lo1le  14589  isercoll  14605  serf0  14618  cvgcmp  14754  dvds1lem  15201  dvds2lem  15202  mulmoddvds  15259  isprm5  15625  vdwlem2  15892  vdwlem10  15900  vdwlem11  15901  lsmcv  19354  lmconst  21285  ptcnplem  21644  fclscmp  22053  tsmsres  22166  addcnlem  22886  lebnumlem3  22981  xlebnum  22983  lebnumii  22984  iscmet3lem2  23308  bcthlem4  23342  cniccbdd  23448  ovoliunlem2  23490  mbfi1flimlem  23708  ply1divex  24115  aalioulem3  24308  aalioulem5  24310  aalioulem6  24311  aaliou  24312  ulmshftlem  24362  ulmbdd  24371  tanarg  24585  cxploglim  24924  ftalem2  25020  ftalem7  25025  dchrisumlem3  25400  frgrogt3nreg  27595  ubthlem3  28067  spansncol  28766  riesz1  29263  erdsze2lem2  31523  dfrdg4  32394  neibastop2  32692  onsuct0  32776  bj-bary1  33498  topdifinffinlem  33531  poimirlem24  33765  incsequz  33875  caushft  33888  equivbnd  33920  cntotbnd  33926  4atexlemex4  35881  frege124d  38579  gneispace  38958  expgrowth  39060  vk15.4j  39259  sstrALT2  39592  iccpartdisj  41898  ccats1pfxeqrex  41947
  Copyright terms: Public domain W3C validator