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

Theorem syl32anc 1219
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 529 . 2  |-  ( ph  ->  ( ta  /\  et ) )
7 syl32anc.6 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ( ta  /\  et ) )  ->  ze )
81, 2, 3, 6, 7syl31anc 1214 1  |-  ( ph  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 958
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 185  df-an 371  df-3an 960
This theorem is referenced by:  coftr  8430  fin1a2s  8571  snunioo  11397  snunico  11398  snunioc  11399  exple1  11906  leexp2rd  12024  facubnd  12059  permnn  12085  dvdsadd2b  13557  dvdsmulgcd  13720  sqgcd  13724  ramlb  14062  0ram  14063  ram0  14065  ramz2  14067  ramz  14068  ramcl  14072  lsmub1x  16124  lsmub2x  16125  lsmsubm  16131  pgpfac1lem2  16549  psrass1lem  17380  psrlidm  17407  psrridm  17409  psrdi  17412  psrdir  17413  psrcom  17414  mplsubrglem  17450  mvrcl  17461  mplcoe2  17480  mplbas2  17482  psrbagev1  17521  psropprmul  17590  xrsdsreclblem  17702  uvcff  18057  uvcresum  18059  frlmup1  18067  smadiadetg  18320  lecldbas  18664  pnfnei  18665  mnfnei  18666  clscon  18875  txcls  19018  ufldom  19376  hauspwpwf1  19401  flfcnp  19418  flfcnp2  19421  cnpfcfi  19454  tsmsmhm  19561  met2ndci  19938  nghmco  20158  nghmplusg  20160  icopnfcld  20188  iocmnfcld  20189  tgioo  20214  reconnlem1  20244  metdseq0  20271  ovolunnul  20824  volinun  20868  volfiniun  20869  volsup  20878  icombl  20886  ioombl  20887  ovolioo  20890  ioorcl2  20893  volivth  20928  ismbf3d  20973  dvferm2lem  21299  lhop  21329  evlslem6  21363  evlslem3  21365  tayl0  21711  pserulm  21771  cxpcn3  22070  ssscongptld  22104  heron  22117  dvdsmulf1o  22418  logexprlim  22448  perfectlem2  22453  lgssq  22558  lgssq2  22559  lgsquad2lem1  22581  lgsquad2lem2  22582  2sqblem  22600  ostth2lem2  22767  ostth3  22771  ubthlem2  24094  nmopleid  25365  numdenneg  25908  archirngz  26029  archiabllem1a  26031  sxbrsigalem2  26554  oddpwdc  26584  ballotlemsdom  26741  ballotlemsel1i  26742  ballotlemsima  26745  ballotlemfrcn0  26759  ismblfin  28273  itg2gt0cn  28288  cntotbnd  28536  ismtyhmeolem  28544  heibor1lem  28549  heiborlem6  28556  rrnequiv  28575  bezoutr  29170  jm2.20nn  29188  jm2.25  29190  kercvrlsm  29278  hashgcdlem  29407  stoweidlem1  29639  stoweidlem20  29658  stoweidlem24  29662  reuccats1  30104  mptscmfsuppd  30630  lincresunit2  30718  1cvrat  32690  ps-2b  32696  2at0mat0  32739  ps-2c  32742  llncvrlpln2  32771  2llnmeqat  32785  4atlem10  32820  4atlem11a  32821  4atlem12a  32824  2lplnja  32833  dalemcea  32874  dalem2  32875  dalem21  32908  dalem54  32940  2lnat  32998  cdlemb  33008  elpaddat  33018  paddasslem7  33040  paddasslem9  33042  paddasslem10  33043  paddasslem15  33048  poml6N  33169  osumcllem6N  33175  osumcllem7N  33176  pexmidlem4N  33187  pl42lem4N  33196  lhplt  33214  lhpjat1  33234  cdlemc5  33409  cdlemeg46fgN  33748  cdlemg12g  33863  tendoco2  33982  tendococl  33986  tendodi1  33998  tendoicl  34010  cdlemi2  34033  tendospdi1  34235  dihord11c  34439  dihmeetlem6  34524  dihjatc1  34526  dihmeetlem10N  34531
  Copyright terms: Public domain W3C validator