MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl32anc Unicode version

Theorem syl32anc 1190
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1  |-  ( ph  ->  ps )
sylXanc.2  |-  ( ph  ->  ch )
sylXanc.3  |-  ( ph  ->  th )
sylXanc.4  |-  ( ph  ->  ta )
sylXanc.5  |-  ( ph  ->  et )
syl32anc.6  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ( ta  /\  et ) )  ->  ze )
Assertion
Ref Expression
syl32anc  |-  ( ph  ->  ze )

Proof of Theorem syl32anc
StepHypRef Expression
1 sylXanc.1 . 2  |-  ( ph  ->  ps )
2 sylXanc.2 . 2  |-  ( ph  ->  ch )
3 sylXanc.3 . 2  |-  ( ph  ->  th )
4 sylXanc.4 . . 3  |-  ( ph  ->  ta )
5 sylXanc.5 . . 3  |-  ( ph  ->  et )
64, 5jca 518 . 2  |-  ( ph  ->  ( ta  /\  et ) )
7 syl32anc.6 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ( ta  /\  et ) )  ->  ze )
81, 2, 3, 6, 7syl31anc 1185 1  |-  ( ph  ->  ze )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  coftr  7899  fin1a2s  8040  snunioo  10762  snunico  10763  exple1  11161  leexp2rd  11278  facubnd  11313  permnn  11336  dvdsadd2b  12571  dvdsmulgcd  12733  sqgcd  12737  ramlb  13066  0ram  13067  ram0  13069  ramz2  13071  ramz  13072  ramcl  13076  lsmub1x  14957  lsmub2x  14958  lsmsubm  14964  pgpfac1lem2  15310  xrsdsreclblem  16417  lecldbas  16949  pnfnei  16950  mnfnei  16951  clscon  17156  txcls  17299  ufldom  17657  hauspwpwf1  17682  flfcnp  17699  flfcnp2  17702  cnpfcfi  17735  tsmsmhm  17828  met2ndci  18068  nghmco  18247  nghmplusg  18249  icopnfcld  18277  iocmnfcld  18278  tgioo  18302  reconnlem1  18331  metdseq0  18358  ovolunnul  18859  volinun  18903  volfiniun  18904  volsup  18913  icombl  18921  ioombl  18922  ovolioo  18925  ioorcl2  18927  volivth  18962  ismbf3d  19009  dvferm2lem  19333  lhop  19363  pserulm  19798  cxpcn3  20088  ssscongptld  20122  dvdsmulf1o  20434  logexprlim  20464  perfectlem2  20469  lgssq  20574  lgssq2  20575  lgsquad2lem1  20597  lgsquad2lem2  20598  2sqblem  20616  ostth2lem2  20783  ostth3  20787  ubthlem2  21450  nmopleid  22719  ballotlemsel1i  23071  ballotlemsima  23074  ballotlemfrcn0  23088  iocinioc2  23272  lmdvg  23376  cntotbnd  26520  ismtyhmeolem  26528  heibor1lem  26533  heiborlem6  26540  rrnequiv  26559  bezoutr  27072  jm2.20nn  27090  jm2.25  27092  kercvrlsm  27181  hashgcdlem  27516  1cvrat  29665  ps-2b  29671  2at0mat0  29714  ps-2c  29717  llncvrlpln2  29746  2llnmeqat  29760  4atlem10  29795  4atlem11a  29796  4atlem12a  29799  2lplnja  29808  dalemcea  29849  dalem2  29850  dalem21  29883  dalem54  29915  2lnat  29973  cdlemb  29983  elpaddat  29993  paddasslem7  30015  paddasslem9  30017  paddasslem10  30018  paddasslem15  30023  poml6N  30144  osumcllem6N  30150  osumcllem7N  30151  pexmidlem4N  30162  pl42lem4N  30171  lhplt  30189  lhpjat1  30209  cdlemc5  30384  cdlemeg46fgN  30723  cdlemg12g  30838  tendoco2  30957  tendococl  30961  tendodi1  30973  tendoicl  30985  cdlemi2  31008  tendospdi1  31210  dihord11c  31414  dihmeetlem6  31499  dihjatc1  31501  dihmeetlem10N  31506
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator