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

Theorem syl6an 680
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 413 . 2 (𝜓 → (𝜃𝜏))
51, 2, 4sylsyld 61 1 (𝜑 → (𝜒𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  dfsb2  2528  dfsb2ALT  2587  xpcan  6027  xpcan2  6028  mapxpen  8672  sucdom2  8703  f1finf1o  8734  unfi  8774  inf3lem3  9082  dfac12r  9561  cfsuc  9668  fin23lem26  9736  iundom2g  9951  inar1  10186  rankcf  10188  ltsrpr  10488  supsrlem  10522  axpre-sup  10580  nominpos  11863  ublbneg  12322  qbtwnre  12582  fsequb  13333  fi1uzind  13845  brfi1indALT  13848  ccats1pfxeqrex  14067  rexanre  14696  rexuzre  14702  rexico  14703  caubnd  14708  rlim2lt  14844  rlim3  14845  lo1bddrp  14872  o1lo1  14884  climshftlem  14921  rlimcn2  14937  rlimo1  14963  lo1add  14973  lo1mul  14974  lo1le  14998  isercoll  15014  serf0  15027  cvgcmp  15161  dvds1lem  15611  dvds2lem  15612  mulmoddvds  15669  isprm5  16041  vdwlem2  16308  vdwlem10  16316  vdwlem11  16317  lsmcv  19844  lmconst  21799  ptcnplem  22159  fclscmp  22568  tsmsres  22681  addcnlem  23401  lebnumlem3  23496  xlebnum  23498  lebnumii  23499  iscmet3lem2  23824  bcthlem4  23859  cniccbdd  23991  ovoliunlem2  24033  mbfi1flimlem  24252  ply1divex  24659  aalioulem3  24852  aalioulem5  24854  aalioulem6  24855  aaliou  24856  ulmshftlem  24906  ulmbdd  24915  tanarg  25129  cxploglim  25483  ftalem2  25579  ftalem7  25584  dchrisumlem3  25995  frgrogt3nreg  28104  ubthlem3  28577  spansncol  29273  riesz1  29770  erdsze2lem2  32349  dfrdg4  33310  neibastop2  33607  onsuct0  33687  bj-bary1  34482  topdifinffinlem  34511  finorwe  34546  poimirlem24  34798  incsequz  34906  caushft  34919  equivbnd  34951  cntotbnd  34957  4atexlemex4  37091  frege124d  39986  gneispace  40364  expgrowth  40547  vk15.4j  40742  sstrALT2  41049  iccpartdisj  43444  fppr2odd  43743
  Copyright terms: Public domain W3C validator