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

Theorem syl32anc 1190
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 518 . 2  |-  ( ph  ->  ( ta  /\  et ) )
7 syl32anc.6 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ( ta  /\  et ) )  ->  ze )
81, 2, 3, 6, 7syl31anc 1185 1  |-  ( ph  ->  ze )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  coftr  7915  fin1a2s  8056  snunioo  10778  snunico  10779  exple1  11177  leexp2rd  11294  facubnd  11329  permnn  11352  dvdsadd2b  12587  dvdsmulgcd  12749  sqgcd  12753  ramlb  13082  0ram  13083  ram0  13085  ramz2  13087  ramz  13088  ramcl  13092  lsmub1x  14973  lsmub2x  14974  lsmsubm  14980  pgpfac1lem2  15326  xrsdsreclblem  16433  lecldbas  16965  pnfnei  16966  mnfnei  16967  clscon  17172  txcls  17315  ufldom  17673  hauspwpwf1  17698  flfcnp  17715  flfcnp2  17718  cnpfcfi  17751  tsmsmhm  17844  met2ndci  18084  nghmco  18263  nghmplusg  18265  icopnfcld  18293  iocmnfcld  18294  tgioo  18318  reconnlem1  18347  metdseq0  18374  ovolunnul  18875  volinun  18919  volfiniun  18920  volsup  18929  icombl  18937  ioombl  18938  ovolioo  18941  ioorcl2  18943  volivth  18978  ismbf3d  19025  dvferm2lem  19349  lhop  19379  pserulm  19814  cxpcn3  20104  ssscongptld  20138  dvdsmulf1o  20450  logexprlim  20480  perfectlem2  20485  lgssq  20590  lgssq2  20591  lgsquad2lem1  20613  lgsquad2lem2  20614  2sqblem  20632  ostth2lem2  20799  ostth3  20803  ubthlem2  21466  nmopleid  22735  ballotlemsel1i  23087  ballotlemsima  23090  ballotlemfrcn0  23104  iocinioc2  23287  lmdvg  23391  itg2gt0cn  25006  cntotbnd  26623  ismtyhmeolem  26631  heibor1lem  26636  heiborlem6  26643  rrnequiv  26662  bezoutr  27175  jm2.20nn  27193  jm2.25  27195  kercvrlsm  27284  hashgcdlem  27619  1cvrat  30287  ps-2b  30293  2at0mat0  30336  ps-2c  30339  llncvrlpln2  30368  2llnmeqat  30382  4atlem10  30417  4atlem11a  30418  4atlem12a  30421  2lplnja  30430  dalemcea  30471  dalem2  30472  dalem21  30505  dalem54  30537  2lnat  30595  cdlemb  30605  elpaddat  30615  paddasslem7  30637  paddasslem9  30639  paddasslem10  30640  paddasslem15  30645  poml6N  30766  osumcllem6N  30772  osumcllem7N  30773  pexmidlem4N  30784  pl42lem4N  30793  lhplt  30811  lhpjat1  30831  cdlemc5  31006  cdlemeg46fgN  31345  cdlemg12g  31460  tendoco2  31579  tendococl  31583  tendodi1  31595  tendoicl  31607  cdlemi2  31630  tendospdi1  31832  dihord11c  32036  dihmeetlem6  32121  dihjatc1  32123  dihmeetlem10N  32128
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator