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

Theorem syl6an 666
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 517 . 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 198  df-an 385
This theorem is referenced by:  dfsb2  2532  xpcan  5781  xpcan2  5782  mapxpen  8365  sucdom2  8395  f1finf1o  8426  unfi  8466  inf3lem3  8774  dfac12r  9253  cfsuc  9364  fin23lem26  9432  iundom2g  9647  inar1  9882  rankcf  9884  ltsrpr  10183  supsrlem  10217  axpre-sup  10275  nominpos  11536  ublbneg  11992  qbtwnre  12248  fsequb  12998  fi1uzind  13496  brfi1indALT  13499  rexanre  14309  rexuzre  14315  rexico  14316  caubnd  14321  rlim2lt  14451  rlim3  14452  lo1bddrp  14479  o1lo1  14491  climshftlem  14528  rlimcn2  14544  rlimo1  14570  lo1add  14580  lo1mul  14581  lo1le  14605  isercoll  14621  serf0  14634  cvgcmp  14770  dvds1lem  15216  dvds2lem  15217  mulmoddvds  15274  isprm5  15636  vdwlem2  15903  vdwlem10  15911  vdwlem11  15912  lsmcv  19349  lmconst  21279  ptcnplem  21638  fclscmp  22047  tsmsres  22160  addcnlem  22880  lebnumlem3  22975  xlebnum  22977  lebnumii  22978  iscmet3lem2  23302  bcthlem4  23336  cniccbdd  23442  ovoliunlem2  23484  mbfi1flimlem  23703  ply1divex  24110  aalioulem3  24303  aalioulem5  24305  aalioulem6  24306  aaliou  24307  ulmshftlem  24357  ulmbdd  24366  tanarg  24579  cxploglim  24918  ftalem2  25014  ftalem7  25019  dchrisumlem3  25394  frgrogt3nreg  27585  ubthlem3  28056  spansncol  28755  riesz1  29252  erdsze2lem2  31509  dfrdg4  32379  neibastop2  32677  onsuct0  32757  bj-bary1  33479  topdifinffinlem  33511  poimirlem24  33746  incsequz  33855  caushft  33868  equivbnd  33900  cntotbnd  33906  4atexlemex4  35853  frege124d  38553  gneispace  38932  expgrowth  39034  vk15.4j  39232  sstrALT2  39564  iccpartdisj  41948  ccats1pfxeqrex  41997
  Copyright terms: Public domain W3C validator