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

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

Proof of Theorem syl32anc
StepHypRef Expression
1 syl3anc.1 . 2 (𝜑𝜓)
2 syl3anc.2 . 2 (𝜑𝜒)
3 syl3anc.3 . 2 (𝜑𝜃)
4 syl3Xanc.4 . . 3 (𝜑𝜏)
5 syl23anc.5 . . 3 (𝜑𝜂)
64, 5jca 512 . 2 (𝜑 → (𝜏𝜂))
7 syl32anc.6 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂)) → 𝜁)
81, 2, 3, 6, 7syl31anc 1365 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  coftr  9684  fin1a2s  9825  ioounsn  12853  snunioo  12854  snunico  12855  snunioc  12856  exple1  13530  leexp2rd  13608  facubnd  13650  permnn  13676  dvdsadd2b  15646  dvdsmulgcd  15895  sqgcd  15899  bezoutr  15902  cncongr2  16002  hashgcdlem  16115  ramlb  16345  0ram  16346  ram0  16348  ramz2  16350  ramz  16351  ramcl  16355  lsmub1x  18702  lsmub2x  18703  lsmsubm  18709  pgpfac1lem2  19128  mptscmfsupp0  19630  psrass1lem  20087  psrlidm  20113  psrridm  20114  psrcom  20119  mplsubrglem  20149  mvrcl  20159  mplcoe5  20179  mplbas2  20181  psrbagev1  20220  evlslem3  20223  evlslem6  20224  psropprmul  20336  xrsdsreclblem  20521  uvcff  20865  uvcresum  20867  frlmup1  20872  smadiadetg  21212  cayhamlem4  21426  lecldbas  21757  pnfnei  21758  mnfnei  21759  clsconn  21968  txcls  22142  ufldom  22500  hauspwpwf1  22525  flfcnp  22542  flfcnp2  22545  cnpfcfi  22578  tsmsmhm  22683  met2ndci  23061  nghmco  23276  nghmplusg  23278  icopnfcld  23305  iocmnfcld  23306  tgioo  23333  reconnlem1  23363  metdseq0  23391  ovolunnul  24030  volinun  24076  volfiniun  24077  volsup  24086  icombl  24094  ioombl  24095  ovolioo  24098  ioorcl2  24102  volivth  24137  ismbf3d  24184  dvferm2lem  24512  lhop  24542  tayl0  24879  pserulm  24939  cxpcn3  25256  ssscongptld  25327  heron  25343  dvdsmulf1o  25699  logexprlim  25729  perfectlem2  25734  lgssq  25841  lgssq2  25842  gausslemma2dlem7  25877  lgsquad2lem1  25888  lgsquad2lem2  25889  2sqblem  25935  2sqcoprm  25939  addsq2nreurex  25948  ostth2lem2  26138  ostth3  26142  ubthlem2  28576  nmopleid  29844  fsuppcurry1  30388  fsuppcurry2  30389  prmdvdsbc  30459  numdenneg  30460  pfxlsw2ccat  30554  wrdt2ind  30555  cyc3conja  30727  archirngz  30746  archiabllem1a  30748  fedgmullem1  30925  fedgmullem2  30926  submatminr1  30975  locfinreflem  31004  sxbrsigalem2  31444  oddpwdc  31512  ballotlemsdom  31669  ballotlemsel1i  31670  ballotlemsima  31673  ballotlemfrcn0  31687  fsum2dsub  31778  circlemeth  31811  elmrsubrn  32665  ismblfin  34815  itg2gt0cn  34829  cntotbnd  34957  ismtyhmeolem  34965  heibor1lem  34970  heiborlem6  34977  rrnequiv  34996  1cvrat  36494  ps-2b  36500  2at0mat0  36543  ps-2c  36546  llncvrlpln2  36575  2llnmeqat  36589  4atlem10  36624  4atlem11a  36625  4atlem12a  36628  2lplnja  36637  dalemcea  36678  dalem2  36679  dalem21  36712  dalem54  36744  2lnat  36802  cdlemb  36812  elpaddat  36822  paddasslem7  36844  paddasslem9  36846  paddasslem10  36847  paddasslem15  36852  poml6N  36973  osumcllem6N  36979  osumcllem7N  36980  pexmidlem4N  36991  pl42lem4N  37000  lhplt  37018  lhpjat1  37038  cdlemc5  37213  cdlemeg46fgN  37552  cdlemg12g  37667  tendoco2  37786  tendococl  37790  tendodi1  37802  tendoicl  37814  cdlemi2  37837  tendospdi1  38038  dihord11c  38242  dihmeetlem6  38327  dihjatc1  38329  dihmeetlem10N  38334  expgcd  39063  fltnltalem  39154  jm2.20nn  39474  jm2.25  39476  kercvrlsm  39563  frege96d  39974  frege98d  39978  ntrclsk3  40300  binomcxplemnn0  40561  snunioo1  41668  limcleqr  41805  dvdivbd  42088  volioc  42137  iblspltprt  42138  volico  42149  stoweidlem1  42167  stoweidlem20  42186  stoweidlem24  42190  etransclem23  42423  iccpartipre  43428  2pwp1prm  43598  perfectALTVlem2  43734  lincresunit2  44431  expnegico01  44471  itscnhlinecirc02plem3  44669
  Copyright terms: Public domain W3C validator