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

Theorem syl6an 568
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 566 . 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  5568  xpcan2  5569  mapxpen  8123  sucdom2  8153  f1finf1o  8184  unfi  8224  inf3lem3  8524  dfac12r  8965  cfsuc  9076  fin23lem26  9144  iundom2g  9359  inar1  9594  rankcf  9596  ltsrpr  9895  supsrlem  9929  axpre-sup  9987  nominpos  11266  ublbneg  11770  qbtwnre  12027  fsequb  12769  fi1uzind  13274  brfi1indALT  13277  fi1uzindOLD  13280  brfi1indALTOLD  13283  rexanre  14080  rexuzre  14086  rexico  14087  caubnd  14092  rlim2lt  14222  rlim3  14223  lo1bddrp  14250  o1lo1  14262  climshftlem  14299  rlimcn2  14315  rlimo1  14341  lo1add  14351  lo1mul  14352  lo1le  14376  isercoll  14392  serf0  14405  cvgcmp  14542  dvds1lem  14987  dvds2lem  14988  isprm5  15413  vdwlem2  15680  vdwlem10  15688  vdwlem11  15689  lsmcv  19135  lmconst  21059  ptcnplem  21418  fclscmp  21828  tsmsres  21941  addcnlem  22661  lebnumlem3  22756  xlebnum  22758  lebnumii  22759  iscmet3lem2  23084  bcthlem4  23118  cniccbdd  23224  ovoliunlem2  23265  mbfi1flimlem  23483  ply1divex  23890  aalioulem3  24083  aalioulem5  24085  aalioulem6  24086  aaliou  24087  ulmshftlem  24137  ulmbdd  24146  tanarg  24359  cxploglim  24698  ftalem2  24794  ftalem7  24799  dchrisumlem3  25174  frgrogt3nreg  27239  ubthlem3  27712  spansncol  28411  riesz1  28908  erdsze2lem2  31171  dfrdg4  32042  neibastop2  32340  onsuct0  32424  bj-bary1  33142  topdifinffinlem  33175  poimirlem24  33413  incsequz  33524  caushft  33537  equivbnd  33569  cntotbnd  33575  4atexlemex4  35185  frege124d  37879  gneispace  38258  expgrowth  38360  vk15.4j  38560  sstrALT2  38896  iccpartdisj  41143  ccats1pfxeqrex  41193
  Copyright terms: Public domain W3C validator