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

Theorem syl6an 567
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 565 . 2 (𝜑 → (𝜒 → (𝜓𝜃)))
4 syl6an.3 . 2 ((𝜓𝜃) → 𝜏)
53, 4syl6 35 1 (𝜑 → (𝜒𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 386
This theorem is referenced by:  dfsb2  2372  xpcan  5534  xpcan2  5535  mapxpen  8077  sucdom2  8107  f1finf1o  8138  unfi  8178  inf3lem3  8478  dfac12r  8919  cfsuc  9030  fin23lem26  9098  iundom2g  9313  inar1  9548  rankcf  9550  ltsrpr  9849  supsrlem  9883  axpre-sup  9941  nominpos  11220  ublbneg  11724  qbtwnre  11980  fsequb  12721  fi1uzind  13225  brfi1indALT  13228  fi1uzindOLD  13231  brfi1indALTOLD  13234  rexanre  14027  rexuzre  14033  rexico  14034  caubnd  14039  rlim2lt  14169  rlim3  14170  lo1bddrp  14197  o1lo1  14209  climshftlem  14246  rlimcn2  14262  rlimo1  14288  lo1add  14298  lo1mul  14299  lo1le  14323  isercoll  14339  serf0  14352  cvgcmp  14482  dvds1lem  14924  dvds2lem  14925  isprm5  15350  vdwlem2  15617  vdwlem10  15625  vdwlem11  15626  lsmcv  19069  lmconst  20984  ptcnplem  21343  fclscmp  21753  tsmsres  21866  addcnlem  22586  lebnumlem3  22681  xlebnum  22683  lebnumii  22684  iscmet3lem2  23009  bcthlem4  23043  cniccbdd  23149  ovoliunlem2  23190  mbfi1flimlem  23408  ply1divex  23813  aalioulem3  24006  aalioulem5  24008  aalioulem6  24009  aaliou  24010  ulmshftlem  24060  ulmbdd  24069  tanarg  24282  cxploglim  24617  ftalem2  24713  ftalem7  24718  dchrisumlem3  25093  frgrogt3nreg  27122  ubthlem3  27595  spansncol  28294  riesz1  28791  erdsze2lem2  30921  dfrdg4  31727  neibastop2  32025  onsuct0  32109  bj-bary1  32822  topdifinffinlem  32854  poimirlem24  33092  incsequz  33203  caushft  33216  equivbnd  33248  cntotbnd  33254  4atexlemex4  34866  frege124d  37561  gneispace  37941  expgrowth  38043  vk15.4j  38243  sstrALT2  38580  iccpartdisj  40692  ccats1pfxeqrex  40742
  Copyright terms: Public domain W3C validator