Theorem syl32anc 1406

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

Step	Hyp	Ref	Expression
1		syl3anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. 2 ⊢ (𝜑 → 𝜃)
4		syl3Xanc.4	. . 3 ⊢ (𝜑 → 𝜏)
5		syl23anc.5	. . 3 ⊢ (𝜑 → 𝜂)
6	4, 5	jca 521	. 2 ⊢ (𝜑 → (𝜏 ∧ 𝜂))
7		syl32anc.6	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁)
8	1, 2, 3, 6, 7	syl31anc 1401	1 ⊢ (𝜑 → 𝜁)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  fsuppsssuppgd  9401  coftr  10378  fin1a2s  10519  ioounsn  13635  snunioo  13636  snunico  13637  snunioc  13638  leexp1ad  14346  exple1  14347  leexp2rd  14426  facubnd  14471  permnn  14497  sqgcd  16765  expgcd  16766  cncongr2  16872  prmdvdsbc  16931  hashgcdlem  16994  ramlb  17226  0ram  17227  ram0  17229  ramz2  17231  ramz  17232  ramcl  17236  lsmub1x  19890  lsmub2x  19891  lsmsubm  19897  pgpfac1lem2  20321  mptscmfsupp0  21232  2idlcpblrng  21595  xrsdsreclblem  21749  pzriprnglem12  21828  uvcff  22127  uvcresum  22129  frlmup1  22134  psrass1lem  22271  psrlidm  22299  psrridm  22300  psrcom  22305  mvrcl  22329  mplsubrglem  22341  mplcoe5  22379  mplbas2  22381  psrbagev1  22416  evlslem3  22419  evlslem6  22420  psropprmul  22585  evls1fpws  22717  smadiadetg  23018  cayhamlem4  23236  lecldbas  23567  pnfnei  23568  mnfnei  23569  clsconn  23778  txcls  23953  ufldom  24311  hauspwpwf1  24336  flfcnp  24353  flfcnp2  24356  cnpfcfi  24389  tsmsmhm  24495  met2ndci  24871  nghmco  25087  nghmplusg  25089  icopnfcld  25116  iocmnfcld  25117  tgioo  25145  reconnlem1  25176  metdseq0  25204  ovolunnul  25851  volinun  25897  volfiniun  25898  volsup  25907  icombl  25915  ioombl  25916  ovolioo  25919  ioorcl2  25923  volivth  25958  ismbf3d  26005  dvferm2lem  26336  lhop  26366  tayl0  26719  pserulm  26779  cxpcn3  27106  ssscongptld  27180  heron  27196  mpodvdsmulf1o  27551  dvdsmulf1o  27553  logexprlim  27582  perfectlem2  27587  lgssq  27694  lgssq2  27695  gausslemma2dlem7  27730  lgsquad2lem1  27741  lgsquad2lem2  27742  2sqblem  27788  addsq2nreurex  27801  ostth2lem2  27991  ostth3  27995  bdayfinbndlem1  28883  ubthlem2  31503  nmopleid  32771  elsuppfnd  33346  fsuppcurry1  33386  fsuppcurry2  33387  znumd  33474  zdend  33475  numdenneg  33476  mgcf1olem1  33632  mgcf1olem2  33633  gsummptres2  33684  archirngz  33820  archiabllem1a  33822  elrgspnlem2  33874  elrgspnlem3  33875  q1pdir  34205  q1pvsca  34206  ply1degltdimlem  34324  fedgmullem1  34331  fedgmullem2  34332  evls1fldgencl  34372  cos9thpiminplylem1  34484  cos9thpiminplylem2  34485  submatminr1  34512  locfinreflem  34542  sxbrsigalem2  34988  elmrsubrn  36452  ismblfin  38771  itg2gt0cn  38785  cntotbnd  38922  ismtyhmeolem  38930  heibor1lem  38935  heiborlem6  38942  rrnequiv  38961  1cvrat  40725  ps-2b  40731  2at0mat0  40774  ps-2c  40777  llncvrlpln2  40806  2llnmeqat  40820  4atlem10  40855  4atlem11a  40856  4atlem12a  40859  2lplnja  40868  dalemcea  40909  dalem2  40910  dalem21  40943  dalem54  40975  2lnat  41033  cdlemb  41043  elpaddat  41053  paddasslem7  41075  paddasslem9  41077  paddasslem10  41078  paddasslem15  41083  poml6N  41204  osumcllem6N  41210  osumcllem7N  41211  pexmidlem4N  41222  pl42lem4N  41231  lhplt  41249  lhpjat1  41269  cdlemc5  41444  cdlemeg46fgN  41783  cdlemg12g  41898  tendoco2  42017  tendococl  42021  tendodi1  42033  tendoicl  42045  cdlemi2  42068  tendospdi1  42269  dihord11c  42473  dihmeetlem6  42558  dihjatc1  42560  dihmeetlem10N  42565  fltnltalem  43866  jm2.20nn  44197  kercvrlsm  44278  omord2lim  44494  frege96d  44941  frege98d  44945  ntrclsk3  45262  snunioo1  46729  limcleqr  46859  dvdivbd  47138  volioc  47187  iblspltprt  47188  volico  47198  stoweidlem1  47216  stoweidlem24  47239  etransclem23  47472  submodlt  48631  iccpartipre  48708  2pwp1prm  48879  perfectALTVlem2  49025  lincresunit2  49795  expnegico01  49835  itscnhlinecirc02plem3  50101