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

Theorem syl32anc 1284
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 539 . 2  |-  ( ph  ->  ( ta  /\  et ) )
7 syl32anc.6 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ( ta  /\  et ) )  ->  ze )
81, 2, 3, 6, 7syl31anc 1279 1  |-  ( ph  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    /\ w3a 991
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 190  df-an 377  df-3an 993
This theorem is referenced by:  coftr  8729  fin1a2s  8870  snunioo  11787  snunico  11788  snunioc  11789  exple1  12364  leexp2rd  12481  facubnd  12517  permnn  12543  reuccats1  12874  dvdsadd2b  14396  dvdsmulgcd  14571  sqgcd  14575  ramlb  15026  0ram  15027  ram0  15029  ramz2  15031  ramz  15032  ramcl  15036  lsmub1x  17347  lsmub2x  17348  lsmsubm  17354  pgpfac1lem2  17757  mptscmfsupp0  18202  psrass1lem  18650  psrlidm  18676  psrridm  18677  psrcom  18682  mplsubrglem  18712  mvrcl  18722  mplcoe5  18741  mplbas2  18743  psrbagev1  18782  evlslem6  18785  evlslem3  18786  psropprmul  18880  xrsdsreclblem  19063  uvcff  19398  uvcresum  19400  frlmup1  19405  smadiadetg  19747  cayhamlem4  19961  lecldbas  20284  pnfnei  20285  mnfnei  20286  clscon  20494  txcls  20668  ufldom  21026  hauspwpwf1  21051  flfcnp  21068  flfcnp2  21071  cnpfcfi  21104  tsmsmhm  21209  met2ndci  21586  nghmco  21808  nghmplusg  21810  icopnfcld  21837  iocmnfcld  21838  tgioo  21863  reconnlem1  21893  metdseq0  21920  metdseq0OLD  21935  ovolunnul  22502  volinun  22548  volfiniun  22549  volsup  22558  icombl  22566  ioombl  22567  ovolioo  22570  ioorcl2  22573  volivth  22614  ismbf3d  22659  dvferm2lem  22987  lhop  23017  tayl0  23366  pserulm  23426  cxpcn3  23737  ssscongptld  23800  heron  23813  dvdsmulf1o  24172  logexprlim  24202  perfectlem2  24207  lgssq  24312  lgssq2  24313  lgsquad2lem1  24335  lgsquad2lem2  24336  2sqblem  24354  ostth2lem2  24521  ostth3  24525  ubthlem2  26562  nmopleid  27841  numdenneg  28429  2sqcoprm  28457  archirngz  28555  archiabllem1a  28557  submatminr1  28685  locfinreflem  28716  sxbrsigalem2  29157  oddpwdc  29236  ballotlemsdom  29393  ballotlemsel1i  29394  ballotlemsima  29397  ballotlemfrcn0  29411  ballotlemsdomOLD  29431  ballotlemsel1iOLD  29432  ballotlemsimaOLD  29435  ballotlemfrcn0OLD  29449  elmrsubrn  30207  ismblfin  32026  itg2gt0cn  32042  cntotbnd  32173  ismtyhmeolem  32181  heibor1lem  32186  heiborlem6  32193  rrnequiv  32212  1cvrat  33086  ps-2b  33092  2at0mat0  33135  ps-2c  33138  llncvrlpln2  33167  2llnmeqat  33181  4atlem10  33216  4atlem11a  33217  4atlem12a  33220  2lplnja  33229  dalemcea  33270  dalem2  33271  dalem21  33304  dalem54  33336  2lnat  33394  cdlemb  33404  elpaddat  33414  paddasslem7  33436  paddasslem9  33438  paddasslem10  33439  paddasslem15  33444  poml6N  33565  osumcllem6N  33571  osumcllem7N  33572  pexmidlem4N  33583  pl42lem4N  33592  lhplt  33610  lhpjat1  33630  cdlemc5  33806  cdlemeg46fgN  34146  cdlemg12g  34261  tendoco2  34380  tendococl  34384  tendodi1  34396  tendoicl  34408  cdlemi2  34431  tendospdi1  34633  dihord11c  34837  dihmeetlem6  34922  dihjatc1  34924  dihmeetlem10N  34929  bezoutr  35880  jm2.20nn  35897  jm2.25  35899  kercvrlsm  35986  hashgcdlem  36119  frege96d  36386  frege98d  36390  binomcxplemnn0  36742  snunioo2  37644  snunioo1  37651  limcleqr  37763  dvdivbd  37833  volioc  37887  iblspltprt  37888  stoweidlem1  37899  stoweidlem20  37918  stoweidlem24  37922  etransclem23  38160  volico  38401  iccpartipre  38773  perfectALTVlem2  38882  lincresunit2  40544  expnegico01  40588
  Copyright terms: Public domain W3C validator