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

Theorem syl32anc 1227
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 1222 1  |-  ( ph  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  coftr  8546  fin1a2s  8687  snunioo  11521  snunico  11522  snunioc  11523  exple1  12033  leexp2rd  12151  facubnd  12186  permnn  12212  dvdsadd2b  13686  dvdsmulgcd  13849  sqgcd  13853  ramlb  14191  0ram  14192  ram0  14194  ramz2  14196  ramz  14197  ramcl  14201  lsmub1x  16258  lsmub2x  16259  lsmsubm  16265  pgpfac1lem2  16690  mptscmfsupp0  17126  psrass1lem  17562  psrlidm  17589  psrridm  17591  psrdi  17594  psrdir  17595  psrcom  17597  mplsubrglem  17633  mvrcl  17644  mplcoe5  17664  mplbas2  17667  psrbagev1  17710  evlslem6  17714  evlslem3  17716  psropprmul  17809  xrsdsreclblem  17977  uvcff  18334  uvcresum  18336  frlmup1  18344  smadiadetg  18604  lecldbas  18948  pnfnei  18949  mnfnei  18950  clscon  19159  txcls  19302  ufldom  19660  hauspwpwf1  19685  flfcnp  19702  flfcnp2  19705  cnpfcfi  19738  tsmsmhm  19845  met2ndci  20222  nghmco  20442  nghmplusg  20444  icopnfcld  20472  iocmnfcld  20473  tgioo  20498  reconnlem1  20528  metdseq0  20555  ovolunnul  21108  volinun  21153  volfiniun  21154  volsup  21163  icombl  21171  ioombl  21172  ovolioo  21175  ioorcl2  21178  volivth  21213  ismbf3d  21258  dvferm2lem  21584  lhop  21614  tayl0  21953  pserulm  22013  cxpcn3  22312  ssscongptld  22346  heron  22359  dvdsmulf1o  22660  logexprlim  22690  perfectlem2  22695  lgssq  22800  lgssq2  22801  lgsquad2lem1  22823  lgsquad2lem2  22824  2sqblem  22842  ostth2lem2  23009  ostth3  23013  ubthlem2  24417  nmopleid  25688  numdenneg  26224  archirngz  26344  archiabllem1a  26346  sxbrsigalem2  26838  oddpwdc  26874  ballotlemsdom  27031  ballotlemsel1i  27032  ballotlemsima  27035  ballotlemfrcn0  27049  ismblfin  28573  itg2gt0cn  28588  cntotbnd  28836  ismtyhmeolem  28844  heibor1lem  28849  heiborlem6  28856  rrnequiv  28875  bezoutr  29469  jm2.20nn  29487  jm2.25  29489  kercvrlsm  29577  hashgcdlem  29706  stoweidlem1  29937  stoweidlem20  29956  stoweidlem24  29960  reuccats1  30402  lincresunit2  31122  pmatcollpw1lem4  31233  1cvrat  33429  ps-2b  33435  2at0mat0  33478  ps-2c  33481  llncvrlpln2  33510  2llnmeqat  33524  4atlem10  33559  4atlem11a  33560  4atlem12a  33563  2lplnja  33572  dalemcea  33613  dalem2  33614  dalem21  33647  dalem54  33679  2lnat  33737  cdlemb  33747  elpaddat  33757  paddasslem7  33779  paddasslem9  33781  paddasslem10  33782  paddasslem15  33787  poml6N  33908  osumcllem6N  33914  osumcllem7N  33915  pexmidlem4N  33926  pl42lem4N  33935  lhplt  33953  lhpjat1  33973  cdlemc5  34148  cdlemeg46fgN  34487  cdlemg12g  34602  tendoco2  34721  tendococl  34725  tendodi1  34737  tendoicl  34749  cdlemi2  34772  tendospdi1  34974  dihord11c  35178  dihmeetlem6  35263  dihjatc1  35265  dihmeetlem10N  35270
  Copyright terms: Public domain W3C validator