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

Theorem syl32anc 1193
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 520 . 2  |-  ( ph  ->  ( ta  /\  et ) )
7 syl32anc.6 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ( ta  /\  et ) )  ->  ze )
81, 2, 3, 6, 7syl31anc 1188 1  |-  ( ph  ->  ze )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  coftr  8158  fin1a2s  8299  snunioo  11028  snunico  11029  exple1  11444  leexp2rd  11561  facubnd  11596  permnn  11622  dvdsadd2b  12897  dvdsmulgcd  13059  sqgcd  13063  ramlb  13392  0ram  13393  ram0  13395  ramz2  13397  ramz  13398  ramcl  13402  lsmub1x  15285  lsmub2x  15286  lsmsubm  15292  pgpfac1lem2  15638  xrsdsreclblem  16749  lecldbas  17288  pnfnei  17289  mnfnei  17290  clscon  17498  txcls  17641  ufldom  17999  hauspwpwf1  18024  flfcnp  18041  flfcnp2  18044  cnpfcfi  18077  tsmsmhm  18180  met2ndci  18557  nghmco  18777  nghmplusg  18779  icopnfcld  18807  iocmnfcld  18808  tgioo  18832  reconnlem1  18862  metdseq0  18889  ovolunnul  19401  volinun  19445  volfiniun  19446  volsup  19455  icombl  19463  ioombl  19464  ovolioo  19467  ioorcl2  19469  volivth  19504  ismbf3d  19549  dvferm2lem  19875  lhop  19905  pserulm  20343  cxpcn3  20637  ssscongptld  20671  dvdsmulf1o  20984  logexprlim  21014  perfectlem2  21019  lgssq  21124  lgssq2  21125  lgsquad2lem1  21147  lgsquad2lem2  21148  2sqblem  21166  ostth2lem2  21333  ostth3  21337  ubthlem2  22378  nmopleid  23647  snunioc  24142  numdenneg  24165  sxbrsigalem2  24641  ballotlemsdom  24774  ballotlemsel1i  24775  ballotlemsima  24778  ballotlemfrcn0  24792  ismblfin  26259  itg2gt0cn  26274  cntotbnd  26519  ismtyhmeolem  26527  heibor1lem  26532  heiborlem6  26539  rrnequiv  26558  bezoutr  27064  jm2.20nn  27082  jm2.25  27084  kercvrlsm  27172  hashgcdlem  27507  stoweidlem1  27740  stoweidlem20  27759  stoweidlem24  27763  1cvrat  30347  ps-2b  30353  2at0mat0  30396  ps-2c  30399  llncvrlpln2  30428  2llnmeqat  30442  4atlem10  30477  4atlem11a  30478  4atlem12a  30481  2lplnja  30490  dalemcea  30531  dalem2  30532  dalem21  30565  dalem54  30597  2lnat  30655  cdlemb  30665  elpaddat  30675  paddasslem7  30697  paddasslem9  30699  paddasslem10  30700  paddasslem15  30705  poml6N  30826  osumcllem6N  30832  osumcllem7N  30833  pexmidlem4N  30844  pl42lem4N  30853  lhplt  30871  lhpjat1  30891  cdlemc5  31066  cdlemeg46fgN  31405  cdlemg12g  31520  tendoco2  31639  tendococl  31643  tendodi1  31655  tendoicl  31667  cdlemi2  31690  tendospdi1  31892  dihord11c  32096  dihmeetlem6  32181  dihjatc1  32183  dihmeetlem10N  32188
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator