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

Theorem syl6an 566
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 564 . 2 (𝜑 → (𝜒 → (𝜓𝜃)))
4 syl6an.3 . 2 ((𝜓𝜃) → 𝜏)
53, 4syl6 34 1 (𝜑 → (𝜒𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 196  df-an 385
This theorem is referenced by:  dfsb2  2361  xpcan  5489  xpcan2  5490  mapxpen  8011  sucdom2  8041  f1finf1o  8072  unfi  8112  inf3lem3  8410  dfac12r  8851  cfsuc  8962  fin23lem26  9030  iundom2g  9241  inar1  9476  rankcf  9478  ltsrpr  9777  supsrlem  9811  axpre-sup  9869  nominpos  11146  ublbneg  11649  qbtwnre  11904  fsequb  12636  fi1uzind  13134  brfi1indALT  13137  fi1uzindOLD  13140  brfi1indALTOLD  13143  rexanre  13934  rexuzre  13940  rexico  13941  caubnd  13946  rlim2lt  14076  rlim3  14077  lo1bddrp  14104  o1lo1  14116  climshftlem  14153  rlimcn2  14169  rlimo1  14195  lo1add  14205  lo1mul  14206  lo1le  14230  isercoll  14246  serf0  14259  cvgcmp  14389  dvds1lem  14831  dvds2lem  14832  isprm5  15257  vdwlem2  15524  vdwlem10  15532  vdwlem11  15533  lsmcv  18962  lmconst  20875  ptcnplem  21234  fclscmp  21644  tsmsres  21757  addcnlem  22475  lebnumlem3  22570  xlebnum  22572  lebnumii  22573  iscmet3lem2  22898  bcthlem4  22932  cniccbdd  23037  ovoliunlem2  23078  mbfi1flimlem  23295  ply1divex  23700  aalioulem3  23893  aalioulem5  23895  aalioulem6  23896  aaliou  23897  ulmshftlem  23947  ulmbdd  23956  tanarg  24169  cxploglim  24504  ftalem2  24600  ftalem7  24605  dchrisumlem3  24980  nvnencycllem  26171  frgraogt3nreg  26647  ubthlem3  27112  spansncol  27811  riesz1  28308  erdsze2lem2  30440  dfrdg4  31228  neibastop2  31526  onsuct0  31610  bj-bary1  32339  topdifinffinlem  32371  poimirlem24  32603  incsequz  32714  caushft  32727  equivbnd  32759  cntotbnd  32765  4atexlemex4  34377  frege124d  37072  gneispace  37452  expgrowth  37556  vk15.4j  37755  sstrALT2  38092  iccpartdisj  39975  ccats1pfxeqrex  40285  av-frgraogt3nreg  41551
  Copyright terms: Public domain W3C validator