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

Theorem syl32anc 1485
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 555 . 2 (𝜑 → (𝜏𝜂))
7 syl32anc.6 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂)) → 𝜁)
81, 2, 3, 6, 7syl31anc 1480 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 385  df-3an 1074
This theorem is referenced by:  coftr  9287  fin1a2s  9428  snunioo  12491  snunico  12492  snunioc  12493  exple1  13114  leexp2rd  13236  facubnd  13281  permnn  13307  reuccats1  13680  dvdsadd2b  15230  dvdsmulgcd  15476  sqgcd  15480  bezoutr  15483  cncongr2  15584  hashgcdlem  15695  ramlb  15925  0ram  15926  ram0  15928  ramz2  15930  ramz  15931  ramcl  15935  lsmub1x  18261  lsmub2x  18262  lsmsubm  18268  pgpfac1lem2  18674  mptscmfsupp0  19130  psrass1lem  19579  psrlidm  19605  psrridm  19606  psrcom  19611  mplsubrglem  19641  mvrcl  19651  mplcoe5  19670  mplbas2  19672  psrbagev1  19712  evlslem6  19715  evlslem3  19716  psropprmul  19810  xrsdsreclblem  19994  uvcff  20332  uvcresum  20334  frlmup1  20339  smadiadetg  20681  cayhamlem4  20895  lecldbas  21225  pnfnei  21226  mnfnei  21227  clsconn  21435  txcls  21609  ufldom  21967  hauspwpwf1  21992  flfcnp  22009  flfcnp2  22012  cnpfcfi  22045  tsmsmhm  22150  met2ndci  22528  nghmco  22743  nghmplusg  22745  icopnfcld  22772  iocmnfcld  22773  tgioo  22800  reconnlem1  22830  metdseq0  22858  ovolunnul  23468  volinun  23514  volfiniun  23515  volsup  23524  icombl  23532  ioombl  23533  ovolioo  23536  ioorcl2  23540  volivth  23575  ismbf3d  23620  dvferm2lem  23948  lhop  23978  tayl0  24315  pserulm  24375  cxpcn3  24688  ssscongptld  24751  heron  24764  dvdsmulf1o  25119  logexprlim  25149  perfectlem2  25154  lgssq  25261  lgssq2  25262  gausslemma2dlem7  25297  lgsquad2lem1  25308  lgsquad2lem2  25309  2sqblem  25355  ostth2lem2  25522  ostth3  25526  ubthlem2  28036  nmopleid  29307  numdenneg  29872  2sqcoprm  29956  archirngz  30052  archiabllem1a  30054  submatminr1  30185  locfinreflem  30216  sxbrsigalem2  30657  oddpwdc  30725  ballotlemsdom  30882  ballotlemsel1i  30883  ballotlemsima  30886  ballotlemfrcn0  30900  fsum2dsub  30994  circlemeth  31027  elmrsubrn  31724  ismblfin  33763  itg2gt0cn  33778  cntotbnd  33908  ismtyhmeolem  33916  heibor1lem  33921  heiborlem6  33928  rrnequiv  33947  1cvrat  35265  ps-2b  35271  2at0mat0  35314  ps-2c  35317  llncvrlpln2  35346  2llnmeqat  35360  4atlem10  35395  4atlem11a  35396  4atlem12a  35399  2lplnja  35408  dalemcea  35449  dalem2  35450  dalem21  35483  dalem54  35515  2lnat  35573  cdlemb  35583  elpaddat  35593  paddasslem7  35615  paddasslem9  35617  paddasslem10  35618  paddasslem15  35623  poml6N  35744  osumcllem6N  35750  osumcllem7N  35751  pexmidlem4N  35762  pl42lem4N  35771  lhplt  35789  lhpjat1  35809  cdlemc5  35985  cdlemeg46fgN  36324  cdlemg12g  36439  tendoco2  36558  tendococl  36562  tendodi1  36574  tendoicl  36586  cdlemi2  36609  tendospdi1  36811  dihord11c  37015  dihmeetlem6  37100  dihjatc1  37102  dihmeetlem10N  37107  jm2.20nn  38066  jm2.25  38068  kercvrlsm  38155  frege96d  38543  frege98d  38547  ntrclsk3  38870  binomcxplemnn0  39050  snunioo2  40234  snunioo1  40241  limcleqr  40379  dvdivbd  40641  volioc  40691  iblspltprt  40692  volico  40703  stoweidlem1  40721  stoweidlem20  40740  stoweidlem24  40744  etransclem23  40977  iccpartipre  41867  2pwp1prm  42013  perfectALTVlem2  42141  lincresunit2  42777  expnegico01  42818
  Copyright terms: Public domain W3C validator