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

Theorem syl6an 671
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 518 . 2 (𝜑 → (𝜒 → (𝜓𝜃)))
4 syl6an.3 . 2 ((𝜓𝜃) → 𝜏)
53, 4syl6 35 1 (𝜑 → (𝜒𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387
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 199  df-an 388
This theorem is referenced by:  dfsb2  2451  dfsb2ALT  2515  xpcan  5871  xpcan2  5872  mapxpen  8475  sucdom2  8505  f1finf1o  8536  unfi  8576  inf3lem3  8883  dfac12r  9362  cfsuc  9473  fin23lem26  9541  iundom2g  9756  inar1  9991  rankcf  9993  ltsrpr  10293  supsrlem  10327  axpre-sup  10385  nominpos  11681  ublbneg  12144  qbtwnre  12406  fsequb  13155  fi1uzind  13660  brfi1indALT  13663  ccats1pfxeqrex  13900  rexanre  14561  rexuzre  14567  rexico  14568  caubnd  14573  rlim2lt  14709  rlim3  14710  lo1bddrp  14737  o1lo1  14749  climshftlem  14786  rlimcn2  14802  rlimo1  14828  lo1add  14838  lo1mul  14839  lo1le  14863  isercoll  14879  serf0  14892  cvgcmp  15025  dvds1lem  15475  dvds2lem  15476  mulmoddvds  15533  isprm5  15901  vdwlem2  16168  vdwlem10  16176  vdwlem11  16177  lsmcv  19629  lmconst  21567  ptcnplem  21927  fclscmp  22336  tsmsres  22449  addcnlem  23169  lebnumlem3  23264  xlebnum  23266  lebnumii  23267  iscmet3lem2  23592  bcthlem4  23627  cniccbdd  23759  ovoliunlem2  23801  mbfi1flimlem  24020  ply1divex  24427  aalioulem3  24620  aalioulem5  24622  aalioulem6  24623  aaliou  24624  ulmshftlem  24674  ulmbdd  24683  tanarg  24897  cxploglim  25251  ftalem2  25347  ftalem7  25352  dchrisumlem3  25763  frgrogt3nreg  27948  ubthlem3  28421  spansncol  29120  riesz1  29617  erdsze2lem2  32026  dfrdg4  32903  neibastop2  33200  onsuct0  33279  bj-bary1  34006  topdifinffinlem  34035  poimirlem24  34335  incsequz  34443  caushft  34456  equivbnd  34488  cntotbnd  34494  4atexlemex4  36632  frege124d  39447  gneispace  39825  expgrowth  40060  vk15.4j  40258  sstrALT2  40565  iccpartdisj  42948  fppr2odd  43238
  Copyright terms: Public domain W3C validator