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

Theorem syl6an 683
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.1 . 2 (𝜑𝜓)
2 syl6an.2 . 2 (𝜑 → (𝜒𝜃))
3 syl6an.3 . . 3 ((𝜓𝜃) → 𝜏)
43ex 416 . 2 (𝜓 → (𝜃𝜏))
51, 2, 4sylsyld 61 1 (𝜑 → (𝜒𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  dfsb2  2514  dfsb2ALT  2570  xpcan  6004  xpcan2  6005  sucdom2  8614  mapxpen  8671  f1finf1o  8733  unfi  8773  inf3lem3  9081  dfac12r  9561  nnadju  9612  cfsuc  9672  fin23lem26  9740  iundom2g  9955  inar1  10190  rankcf  10192  ltsrpr  10492  supsrlem  10526  axpre-sup  10584  nominpos  11866  ublbneg  12325  qbtwnre  12584  fsequb  13342  fi1uzind  13855  brfi1indALT  13858  ccats1pfxeqrex  14072  rexanre  14702  rexuzre  14708  rexico  14709  caubnd  14714  rlim2lt  14850  rlim3  14851  lo1bddrp  14878  o1lo1  14890  climshftlem  14927  rlimcn2  14943  rlimo1  14969  lo1add  14979  lo1mul  14980  lo1le  15004  isercoll  15020  serf0  15033  cvgcmp  15167  dvds1lem  15617  dvds2lem  15618  mulmoddvds  15675  isprm5  16045  vdwlem2  16312  vdwlem10  16320  vdwlem11  16321  lsmcv  19910  lmconst  21870  ptcnplem  22230  fclscmp  22639  tsmsres  22753  addcnlem  23473  lebnumlem3  23572  xlebnum  23574  lebnumii  23575  iscmet3lem2  23900  bcthlem4  23935  cniccbdd  24069  ovoliunlem2  24111  mbfi1flimlem  24330  ply1divex  24741  aalioulem3  24934  aalioulem5  24936  aalioulem6  24937  aaliou  24938  ulmshftlem  24988  ulmbdd  24997  tanarg  25214  cxploglim  25567  ftalem2  25663  ftalem7  25668  dchrisumlem3  26079  frgrogt3nreg  28186  ubthlem3  28659  spansncol  29355  riesz1  29852  erdsze2lem2  32565  dfrdg4  33526  neibastop2  33823  onsuct0  33903  bj-bary1  34727  topdifinffinlem  34765  finorwe  34800  poimirlem24  35080  incsequz  35185  caushft  35198  equivbnd  35227  cntotbnd  35233  4atexlemex4  37368  frege124d  40455  gneispace  40830  expgrowth  41032  vk15.4j  41227  sstrALT2  41534  iccpartdisj  43947  fppr2odd  44242
  Copyright terms: Public domain W3C validator