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

Theorem syl32anc 1272
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 534 . 2  |-  ( ph  ->  ( ta  /\  et ) )
7 syl32anc.6 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ( ta  /\  et ) )  ->  ze )
81, 2, 3, 6, 7syl31anc 1267 1  |-  ( ph  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  coftr  8703  fin1a2s  8844  snunioo  11758  snunico  11759  snunioc  11760  exple1  12331  leexp2rd  12448  facubnd  12484  permnn  12510  reuccats1  12827  dvdsadd2b  14334  dvdsmulgcd  14509  sqgcd  14513  ramlb  14964  0ram  14965  ram0  14967  ramz2  14969  ramz  14970  ramcl  14974  lsmub1x  17285  lsmub2x  17286  lsmsubm  17292  pgpfac1lem2  17695  mptscmfsupp0  18140  psrass1lem  18588  psrlidm  18614  psrridm  18615  psrcom  18620  mplsubrglem  18650  mvrcl  18660  mplcoe5  18679  mplbas2  18681  psrbagev1  18720  evlslem6  18723  evlslem3  18724  psropprmul  18818  xrsdsreclblem  19001  uvcff  19335  uvcresum  19337  frlmup1  19342  smadiadetg  19684  cayhamlem4  19898  lecldbas  20221  pnfnei  20222  mnfnei  20223  clscon  20431  txcls  20605  ufldom  20963  hauspwpwf1  20988  flfcnp  21005  flfcnp2  21008  cnpfcfi  21041  tsmsmhm  21146  met2ndci  21523  nghmco  21745  nghmplusg  21747  icopnfcld  21774  iocmnfcld  21775  tgioo  21800  reconnlem1  21830  metdseq0  21857  metdseq0OLD  21872  ovolunnul  22439  volinun  22485  volfiniun  22486  volsup  22495  icombl  22503  ioombl  22504  ovolioo  22507  ioorcl2  22510  volivth  22551  ismbf3d  22596  dvferm2lem  22924  lhop  22954  tayl0  23303  pserulm  23363  cxpcn3  23674  ssscongptld  23737  heron  23750  dvdsmulf1o  24109  logexprlim  24139  perfectlem2  24144  lgssq  24249  lgssq2  24250  lgsquad2lem1  24272  lgsquad2lem2  24273  2sqblem  24291  ostth2lem2  24458  ostth3  24462  ubthlem2  26498  nmopleid  27777  numdenneg  28374  2sqcoprm  28402  archirngz  28500  archiabllem1a  28502  submatminr1  28631  locfinreflem  28662  sxbrsigalem2  29103  oddpwdc  29182  ballotlemsdom  29339  ballotlemsel1i  29340  ballotlemsima  29343  ballotlemfrcn0  29357  ballotlemsdomOLD  29377  ballotlemsel1iOLD  29378  ballotlemsimaOLD  29381  ballotlemfrcn0OLD  29395  elmrsubrn  30153  ismblfin  31894  itg2gt0cn  31910  cntotbnd  32041  ismtyhmeolem  32049  heibor1lem  32054  heiborlem6  32061  rrnequiv  32080  1cvrat  32959  ps-2b  32965  2at0mat0  33008  ps-2c  33011  llncvrlpln2  33040  2llnmeqat  33054  4atlem10  33089  4atlem11a  33090  4atlem12a  33093  2lplnja  33102  dalemcea  33143  dalem2  33144  dalem21  33177  dalem54  33209  2lnat  33267  cdlemb  33277  elpaddat  33287  paddasslem7  33309  paddasslem9  33311  paddasslem10  33312  paddasslem15  33317  poml6N  33438  osumcllem6N  33444  osumcllem7N  33445  pexmidlem4N  33456  pl42lem4N  33465  lhplt  33483  lhpjat1  33503  cdlemc5  33679  cdlemeg46fgN  34019  cdlemg12g  34134  tendoco2  34253  tendococl  34257  tendodi1  34269  tendoicl  34281  cdlemi2  34304  tendospdi1  34506  dihord11c  34710  dihmeetlem6  34795  dihjatc1  34797  dihmeetlem10N  34802  bezoutr  35754  jm2.20nn  35771  jm2.25  35773  kercvrlsm  35860  hashgcdlem  35993  frege96d  36200  frege98d  36204  binomcxplemnn0  36555  snunioo2  37436  snunioo1  37443  limcleqr  37544  dvdivbd  37614  volioc  37668  iblspltprt  37669  stoweidlem1  37680  stoweidlem20  37699  stoweidlem24  37703  etransclem23  37941  volico  38137  iccpartipre  38446  perfectALTVlem2  38555  lincresunit2  39544  expnegico01  39588
  Copyright terms: Public domain W3C validator