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

Theorem syl32anc 1192
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 519 . 2  |-  ( ph  ->  ( ta  /\  et ) )
7 syl32anc.6 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ( ta  /\  et ) )  ->  ze )
81, 2, 3, 6, 7syl31anc 1187 1  |-  ( ph  ->  ze )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  coftr  8145  fin1a2s  8286  snunioo  11015  snunico  11016  exple1  11431  leexp2rd  11548  facubnd  11583  permnn  11609  dvdsadd2b  12884  dvdsmulgcd  13046  sqgcd  13050  ramlb  13379  0ram  13380  ram0  13382  ramz2  13384  ramz  13385  ramcl  13389  lsmub1x  15272  lsmub2x  15273  lsmsubm  15279  pgpfac1lem2  15625  xrsdsreclblem  16736  lecldbas  17275  pnfnei  17276  mnfnei  17277  clscon  17485  txcls  17628  ufldom  17986  hauspwpwf1  18011  flfcnp  18028  flfcnp2  18031  cnpfcfi  18064  tsmsmhm  18167  met2ndci  18544  nghmco  18764  nghmplusg  18766  icopnfcld  18794  iocmnfcld  18795  tgioo  18819  reconnlem1  18849  metdseq0  18876  ovolunnul  19388  volinun  19432  volfiniun  19433  volsup  19442  icombl  19450  ioombl  19451  ovolioo  19454  ioorcl2  19456  volivth  19491  ismbf3d  19538  dvferm2lem  19862  lhop  19892  pserulm  20330  cxpcn3  20624  ssscongptld  20658  dvdsmulf1o  20971  logexprlim  21001  perfectlem2  21006  lgssq  21111  lgssq2  21112  lgsquad2lem1  21134  lgsquad2lem2  21135  2sqblem  21153  ostth2lem2  21320  ostth3  21324  ubthlem2  22365  nmopleid  23634  snunioc  24129  numdenneg  24152  sxbrsigalem2  24628  ballotlemsdom  24761  ballotlemsel1i  24762  ballotlemsima  24765  ballotlemfrcn0  24779  ismblfin  26237  itg2gt0cn  26250  cntotbnd  26496  ismtyhmeolem  26504  heibor1lem  26509  heiborlem6  26516  rrnequiv  26535  bezoutr  27041  jm2.20nn  27059  jm2.25  27061  kercvrlsm  27149  hashgcdlem  27484  stoweidlem1  27717  stoweidlem20  27736  stoweidlem24  27740  1cvrat  30210  ps-2b  30216  2at0mat0  30259  ps-2c  30262  llncvrlpln2  30291  2llnmeqat  30305  4atlem10  30340  4atlem11a  30341  4atlem12a  30344  2lplnja  30353  dalemcea  30394  dalem2  30395  dalem21  30428  dalem54  30460  2lnat  30518  cdlemb  30528  elpaddat  30538  paddasslem7  30560  paddasslem9  30562  paddasslem10  30563  paddasslem15  30568  poml6N  30689  osumcllem6N  30695  osumcllem7N  30696  pexmidlem4N  30707  pl42lem4N  30716  lhplt  30734  lhpjat1  30754  cdlemc5  30929  cdlemeg46fgN  31268  cdlemg12g  31383  tendoco2  31502  tendococl  31506  tendodi1  31518  tendoicl  31530  cdlemi2  31553  tendospdi1  31755  dihord11c  31959  dihmeetlem6  32044  dihjatc1  32046  dihmeetlem10N  32051
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator