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

Theorem syl32anc 1484
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
syl12anc.1 (𝜑𝜓)
syl12anc.2 (𝜑𝜒)
syl12anc.3 (𝜑𝜃)
syl22anc.4 (𝜑𝜏)
syl23anc.5 (𝜑𝜂)
syl32anc.6 (((𝜓𝜒𝜃) ∧ (𝜏𝜂)) → 𝜁)
Assertion
Ref Expression
syl32anc (𝜑𝜁)

Proof of Theorem syl32anc
StepHypRef Expression
1 syl12anc.1 . 2 (𝜑𝜓)
2 syl12anc.2 . 2 (𝜑𝜒)
3 syl12anc.3 . 2 (𝜑𝜃)
4 syl22anc.4 . . 3 (𝜑𝜏)
5 syl23anc.5 . . 3 (𝜑𝜂)
64, 5jca 501 . 2 (𝜑 → (𝜏𝜂))
7 syl32anc.6 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂)) → 𝜁)
81, 2, 3, 6, 7syl31anc 1479 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071
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 197  df-an 383  df-3an 1073
This theorem is referenced by:  coftr  9297  fin1a2s  9438  snunioo  12505  snunico  12506  snunioc  12507  exple1  13127  leexp2rd  13249  facubnd  13291  permnn  13317  reuccats1  13689  dvdsadd2b  15237  dvdsmulgcd  15482  sqgcd  15486  bezoutr  15489  cncongr2  15589  hashgcdlem  15700  ramlb  15930  0ram  15931  ram0  15933  ramz2  15935  ramz  15936  ramcl  15940  lsmub1x  18268  lsmub2x  18269  lsmsubm  18275  pgpfac1lem2  18682  mptscmfsupp0  19138  psrass1lem  19592  psrlidm  19618  psrridm  19619  psrcom  19624  mplsubrglem  19654  mvrcl  19664  mplcoe5  19683  mplbas2  19685  psrbagev1  19725  evlslem6  19728  evlslem3  19729  psropprmul  19823  xrsdsreclblem  20007  uvcff  20347  uvcresum  20349  frlmup1  20354  smadiadetg  20698  cayhamlem4  20913  lecldbas  21244  pnfnei  21245  mnfnei  21246  clsconn  21454  txcls  21628  ufldom  21986  hauspwpwf1  22011  flfcnp  22028  flfcnp2  22031  cnpfcfi  22064  tsmsmhm  22169  met2ndci  22547  nghmco  22762  nghmplusg  22764  icopnfcld  22791  iocmnfcld  22792  tgioo  22819  reconnlem1  22849  metdseq0  22877  ovolunnul  23488  volinun  23534  volfiniun  23535  volsup  23544  icombl  23552  ioombl  23553  ovolioo  23556  ioorcl2  23560  volivth  23595  ismbf3d  23641  dvferm2lem  23969  lhop  23999  tayl0  24336  pserulm  24396  cxpcn3  24710  ssscongptld  24773  heron  24786  dvdsmulf1o  25141  logexprlim  25171  perfectlem2  25176  lgssq  25283  lgssq2  25284  gausslemma2dlem7  25319  lgsquad2lem1  25330  lgsquad2lem2  25331  2sqblem  25377  ostth2lem2  25544  ostth3  25548  ubthlem2  28067  nmopleid  29338  numdenneg  29903  2sqcoprm  29987  archirngz  30083  archiabllem1a  30085  submatminr1  30216  locfinreflem  30247  sxbrsigalem2  30688  oddpwdc  30756  ballotlemsdom  30913  ballotlemsel1i  30914  ballotlemsima  30917  ballotlemfrcn0  30931  fsum2dsub  31025  circlemeth  31058  elmrsubrn  31755  ismblfin  33783  itg2gt0cn  33797  cntotbnd  33927  ismtyhmeolem  33935  heibor1lem  33940  heiborlem6  33947  rrnequiv  33966  1cvrat  35284  ps-2b  35290  2at0mat0  35333  ps-2c  35336  llncvrlpln2  35365  2llnmeqat  35379  4atlem10  35414  4atlem11a  35415  4atlem12a  35418  2lplnja  35427  dalemcea  35468  dalem2  35469  dalem21  35502  dalem54  35534  2lnat  35592  cdlemb  35602  elpaddat  35612  paddasslem7  35634  paddasslem9  35636  paddasslem10  35637  paddasslem15  35642  poml6N  35763  osumcllem6N  35769  osumcllem7N  35770  pexmidlem4N  35781  pl42lem4N  35790  lhplt  35808  lhpjat1  35828  cdlemc5  36004  cdlemeg46fgN  36343  cdlemg12g  36458  tendoco2  36577  tendococl  36581  tendodi1  36593  tendoicl  36605  cdlemi2  36628  tendospdi1  36830  dihord11c  37034  dihmeetlem6  37119  dihjatc1  37121  dihmeetlem10N  37126  jm2.20nn  38090  jm2.25  38092  kercvrlsm  38179  frege96d  38567  frege98d  38571  ntrclsk3  38894  binomcxplemnn0  39074  snunioo2  40252  snunioo1  40257  limcleqr  40394  dvdivbd  40656  volioc  40705  iblspltprt  40706  volico  40717  stoweidlem1  40735  stoweidlem20  40754  stoweidlem24  40758  etransclem23  40991  iccpartipre  41885  2pwp1prm  42031  perfectALTVlem2  42159  lincresunit2  42795  expnegico01  42836
  Copyright terms: Public domain W3C validator