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

Theorem syl6an 655
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 509 . 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  2519  xpcan  5711  xpcan2  5712  mapxpen  8281  sucdom2  8311  f1finf1o  8342  unfi  8382  inf3lem3  8690  dfac12r  9169  cfsuc  9280  fin23lem26  9348  iundom2g  9563  inar1  9798  rankcf  9800  ltsrpr  10099  supsrlem  10133  axpre-sup  10191  nominpos  11470  ublbneg  11975  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  27590  ubthlem3  28062  spansncol  28761  riesz1  29258  erdsze2lem2  31518  dfrdg4  32389  neibastop2  32687  onsuct0  32771  bj-bary1  33492  topdifinffinlem  33525  poimirlem24  33759  incsequz  33869  caushft  33882  equivbnd  33914  cntotbnd  33920  4atexlemex4  35874  frege124d  38572  gneispace  38951  expgrowth  39053  vk15.4j  39253  sstrALT2  39586  iccpartdisj  41891  ccats1pfxeqrex  41940
  Copyright terms: Public domain W3C validator