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  8670  fin1a2s  8811  snunioo  11671  snunico  11672  snunioc  11673  exple1  12228  leexp2rd  12346  facubnd  12381  permnn  12407  reuccats1  12718  dvdsadd2b  14040  dvdsmulgcd  14204  sqgcd  14208  ramlb  14549  0ram  14550  ram0  14552  ramz2  14554  ramz  14555  ramcl  14559  lsmub1x  16793  lsmub2x  16794  lsmsubm  16800  pgpfac1lem2  17253  mptscmfsupp0  17703  psrass1lem  18156  psrlidm  18183  psrridm  18185  psrcom  18191  mplsubrglem  18227  mvrcl  18238  mplcoe5  18258  mplbas2  18261  psrbagev1  18304  evlslem6  18308  evlslem3  18310  psropprmul  18406  xrsdsreclblem  18591  uvcff  18949  uvcresum  18951  frlmup1  18959  smadiadetg  19302  cayhamlem4  19516  lecldbas  19847  pnfnei  19848  mnfnei  19849  clscon  20057  txcls  20231  ufldom  20589  hauspwpwf1  20614  flfcnp  20631  flfcnp2  20634  cnpfcfi  20667  tsmsmhm  20774  met2ndci  21151  nghmco  21371  nghmplusg  21373  icopnfcld  21401  iocmnfcld  21402  tgioo  21427  reconnlem1  21457  metdseq0  21484  ovolunnul  22037  volinun  22082  volfiniun  22083  volsup  22092  icombl  22100  ioombl  22101  ovolioo  22104  ioorcl2  22107  volivth  22142  ismbf3d  22187  dvferm2lem  22513  lhop  22543  tayl0  22883  pserulm  22943  cxpcn3  23248  ssscongptld  23282  heron  23295  dvdsmulf1o  23596  logexprlim  23626  perfectlem2  23631  lgssq  23736  lgssq2  23737  lgsquad2lem1  23759  lgsquad2lem2  23760  2sqblem  23778  ostth2lem2  23945  ostth3  23949  ubthlem2  25914  nmopleid  27185  numdenneg  27768  2sqcoprm  27795  archirngz  27893  archiabllem1a  27895  locfinreflem  28004  sxbrsigalem2  28430  oddpwdc  28490  ballotlemsdom  28647  ballotlemsel1i  28648  ballotlemsima  28651  ballotlemfrcn0  28665  elmrsubrn  29077  ismblfin  30260  itg2gt0cn  30275  cntotbnd  30497  ismtyhmeolem  30505  heibor1lem  30510  heiborlem6  30517  rrnequiv  30536  bezoutr  31127  jm2.20nn  31143  jm2.25  31145  kercvrlsm  31233  hashgcdlem  31361  binomcxplemnn0  31458  snunioo2  31747  snunioo1  31755  limcleqr  31853  dvdivbd  31923  volioc  31974  iblspltprt  31975  stoweidlem1  31986  stoweidlem20  32005  stoweidlem24  32009  etransclem23  32243  lincresunit2  33223  1cvrat  35343  ps-2b  35349  2at0mat0  35392  ps-2c  35395  llncvrlpln2  35424  2llnmeqat  35438  4atlem10  35473  4atlem11a  35474  4atlem12a  35477  2lplnja  35486  dalemcea  35527  dalem2  35528  dalem21  35561  dalem54  35593  2lnat  35651  cdlemb  35661  elpaddat  35671  paddasslem7  35693  paddasslem9  35695  paddasslem10  35696  paddasslem15  35701  poml6N  35822  osumcllem6N  35828  osumcllem7N  35829  pexmidlem4N  35840  pl42lem4N  35849  lhplt  35867  lhpjat1  35887  cdlemc5  36063  cdlemeg46fgN  36403  cdlemg12g  36518  tendoco2  36637  tendococl  36641  tendodi1  36653  tendoicl  36665  cdlemi2  36688  tendospdi1  36890  dihord11c  37094  dihmeetlem6  37179  dihjatc1  37181  dihmeetlem10N  37186
  Copyright terms: Public domain W3C validator