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

Theorem syl32anc 1326
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 553 . 2 (𝜑 → (𝜏𝜂))
7 syl32anc.6 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂)) → 𝜁)
81, 2, 3, 6, 7syl31anc 1321 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  coftr  8978  fin1a2s  9119  snunioo  12169  snunico  12170  snunioc  12171  exple1  12782  leexp2rd  12904  facubnd  12949  permnn  12975  reuccats1  13332  dvdsadd2b  14866  dvdsmulgcd  15112  sqgcd  15116  bezoutr  15119  cncongr2  15220  hashgcdlem  15331  ramlb  15561  0ram  15562  ram0  15564  ramz2  15566  ramz  15567  ramcl  15571  lsmub1x  17884  lsmub2x  17885  lsmsubm  17891  pgpfac1lem2  18297  mptscmfsupp0  18751  psrass1lem  19198  psrlidm  19224  psrridm  19225  psrcom  19230  mplsubrglem  19260  mvrcl  19270  mplcoe5  19289  mplbas2  19291  psrbagev1  19331  evlslem6  19334  evlslem3  19335  psropprmul  19429  xrsdsreclblem  19611  uvcff  19949  uvcresum  19951  frlmup1  19956  smadiadetg  20298  cayhamlem4  20512  lecldbas  20833  pnfnei  20834  mnfnei  20835  clscon  21043  txcls  21217  ufldom  21576  hauspwpwf1  21601  flfcnp  21618  flfcnp2  21621  cnpfcfi  21654  tsmsmhm  21759  met2ndci  22137  nghmco  22352  nghmplusg  22354  icopnfcld  22381  iocmnfcld  22382  tgioo  22407  reconnlem1  22437  metdseq0  22465  ovolunnul  23075  volinun  23121  volfiniun  23122  volsup  23131  icombl  23139  ioombl  23140  ovolioo  23143  ioorcl2  23146  volivth  23181  ismbf3d  23227  dvferm2lem  23553  lhop  23583  tayl0  23920  pserulm  23980  cxpcn3  24289  ssscongptld  24352  heron  24365  dvdsmulf1o  24720  logexprlim  24750  perfectlem2  24755  lgssq  24862  lgssq2  24863  gausslemma2dlem7  24898  lgsquad2lem1  24909  lgsquad2lem2  24910  2sqblem  24956  ostth2lem2  25123  ostth3  25127  ubthlem2  27111  nmopleid  28382  numdenneg  28950  2sqcoprm  28978  archirngz  29074  archiabllem1a  29076  submatminr1  29204  locfinreflem  29235  sxbrsigalem2  29675  oddpwdc  29743  ballotlemsdom  29900  ballotlemsel1i  29901  ballotlemsima  29904  ballotlemfrcn0  29918  elmrsubrn  30671  ismblfin  32620  itg2gt0cn  32635  cntotbnd  32765  ismtyhmeolem  32773  heibor1lem  32778  heiborlem6  32785  rrnequiv  32804  1cvrat  33780  ps-2b  33786  2at0mat0  33829  ps-2c  33832  llncvrlpln2  33861  2llnmeqat  33875  4atlem10  33910  4atlem11a  33911  4atlem12a  33914  2lplnja  33923  dalemcea  33964  dalem2  33965  dalem21  33998  dalem54  34030  2lnat  34088  cdlemb  34098  elpaddat  34108  paddasslem7  34130  paddasslem9  34132  paddasslem10  34133  paddasslem15  34138  poml6N  34259  osumcllem6N  34265  osumcllem7N  34266  pexmidlem4N  34277  pl42lem4N  34286  lhplt  34304  lhpjat1  34324  cdlemc5  34500  cdlemeg46fgN  34840  cdlemg12g  34955  tendoco2  35074  tendococl  35078  tendodi1  35090  tendoicl  35102  cdlemi2  35125  tendospdi1  35327  dihord11c  35531  dihmeetlem6  35616  dihjatc1  35618  dihmeetlem10N  35623  jm2.20nn  36582  jm2.25  36584  kercvrlsm  36671  frege96d  37060  frege98d  37064  ntrclsk3  37388  binomcxplemnn0  37570  snunioo2  38578  snunioo1  38585  limcleqr  38711  dvdivbd  38813  volioc  38864  iblspltprt  38865  volico  38876  stoweidlem1  38894  stoweidlem20  38913  stoweidlem24  38917  etransclem23  39150  iccpartipre  39959  2pwp1prm  40041  perfectALTVlem2  40165  lincresunit2  42061  expnegico01  42102
  Copyright terms: Public domain W3C validator