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

Theorem syl32anc 1236
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 532 . 2  |-  ( ph  ->  ( ta  /\  et ) )
7 syl32anc.6 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ( ta  /\  et ) )  ->  ze )
81, 2, 3, 6, 7syl31anc 1231 1  |-  ( ph  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 975
This theorem is referenced by:  coftr  8649  fin1a2s  8790  snunioo  11642  snunico  11643  snunioc  11644  exple1  12189  leexp2rd  12307  facubnd  12342  permnn  12368  reuccats1  12665  dvdsadd2b  13883  dvdsmulgcd  14047  sqgcd  14051  ramlb  14392  0ram  14393  ram0  14395  ramz2  14397  ramz  14398  ramcl  14402  lsmub1x  16462  lsmub2x  16463  lsmsubm  16469  pgpfac1lem2  16916  mptscmfsupp0  17359  psrass1lem  17800  psrlidm  17827  psrridm  17829  psrdi  17832  psrdir  17833  psrcom  17835  mplsubrglem  17871  mvrcl  17882  mplcoe5  17902  mplbas2  17905  psrbagev1  17948  evlslem6  17952  evlslem3  17954  psropprmul  18050  xrsdsreclblem  18232  uvcff  18589  uvcresum  18591  frlmup1  18599  smadiadetg  18942  cayhamlem4  19156  lecldbas  19486  pnfnei  19487  mnfnei  19488  clscon  19697  txcls  19840  ufldom  20198  hauspwpwf1  20223  flfcnp  20240  flfcnp2  20243  cnpfcfi  20276  tsmsmhm  20383  met2ndci  20760  nghmco  20980  nghmplusg  20982  icopnfcld  21010  iocmnfcld  21011  tgioo  21036  reconnlem1  21066  metdseq0  21093  ovolunnul  21646  volinun  21691  volfiniun  21692  volsup  21701  icombl  21709  ioombl  21710  ovolioo  21713  ioorcl2  21716  volivth  21751  ismbf3d  21796  dvferm2lem  22122  lhop  22152  tayl0  22491  pserulm  22551  cxpcn3  22850  ssscongptld  22884  heron  22897  dvdsmulf1o  23198  logexprlim  23228  perfectlem2  23233  lgssq  23338  lgssq2  23339  lgsquad2lem1  23361  lgsquad2lem2  23362  2sqblem  23380  ostth2lem2  23547  ostth3  23551  ubthlem2  25463  nmopleid  26734  numdenneg  27275  archirngz  27395  archiabllem1a  27397  sxbrsigalem2  27897  oddpwdc  27933  ballotlemsdom  28090  ballotlemsel1i  28091  ballotlemsima  28094  ballotlemfrcn0  28108  ismblfin  29632  itg2gt0cn  29647  cntotbnd  29895  ismtyhmeolem  29903  heibor1lem  29908  heiborlem6  29915  rrnequiv  29934  bezoutr  30527  jm2.20nn  30543  jm2.25  30545  kercvrlsm  30633  hashgcdlem  30762  snunioo2  31108  snunioo1  31116  limcleqr  31186  dvdivbd  31253  stoweidlem1  31301  stoweidlem20  31320  stoweidlem24  31324  lincresunit2  32152  1cvrat  34272  ps-2b  34278  2at0mat0  34321  ps-2c  34324  llncvrlpln2  34353  2llnmeqat  34367  4atlem10  34402  4atlem11a  34403  4atlem12a  34406  2lplnja  34415  dalemcea  34456  dalem2  34457  dalem21  34490  dalem54  34522  2lnat  34580  cdlemb  34590  elpaddat  34600  paddasslem7  34622  paddasslem9  34624  paddasslem10  34625  paddasslem15  34630  poml6N  34751  osumcllem6N  34757  osumcllem7N  34758  pexmidlem4N  34769  pl42lem4N  34778  lhplt  34796  lhpjat1  34816  cdlemc5  34991  cdlemeg46fgN  35330  cdlemg12g  35445  tendoco2  35564  tendococl  35568  tendodi1  35580  tendoicl  35592  cdlemi2  35615  tendospdi1  35817  dihord11c  36021  dihmeetlem6  36106  dihjatc1  36108  dihmeetlem10N  36113
  Copyright terms: Public domain W3C validator