Theorem syl32anc 1380

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 511	. 2 ⊢ (𝜑 → (𝜏 ∧ 𝜂))
7		syl32anc.6	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁)
8	1, 2, 3, 6, 7	syl31anc 1375	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  fsuppsssuppgd  9392  coftr  10285  fin1a2s  10426  ioounsn  13492  snunioo  13493  snunico  13494  snunioc  13495  leexp1ad  14192  exple1  14193  leexp2rd  14271  facubnd  14316  permnn  14342  sqgcd  16579  expgcd  16580  cncongr2  16685  prmdvdsbc  16743  hashgcdlem  16805  ramlb  17037  0ram  17038  ram0  17040  ramz2  17042  ramz  17043  ramcl  17047  lsmub1x  19625  lsmub2x  19626  lsmsubm  19632  pgpfac1lem2  20056  mptscmfsupp0  20882  2idlcpblrng  21230  xrsdsreclblem  21378  pzriprnglem12  21451  uvcff  21749  uvcresum  21751  frlmup1  21756  psrass1lem  21890  psrlidm  21920  psrridm  21921  psrcom  21926  mvrcl  21950  mplsubrglem  21962  mplcoe5  21996  mplbas2  21998  psrbagev1  22033  evlslem3  22036  evlslem6  22037  psropprmul  22171  evls1fpws  22305  smadiadetg  22609  cayhamlem4  22824  lecldbas  23155  pnfnei  23156  mnfnei  23157  clsconn  23366  txcls  23540  ufldom  23898  hauspwpwf1  23923  flfcnp  23940  flfcnp2  23943  cnpfcfi  23976  tsmsmhm  24082  met2ndci  24459  nghmco  24675  nghmplusg  24677  icopnfcld  24704  iocmnfcld  24705  tgioo  24733  reconnlem1  24764  metdseq0  24792  ovolunnul  25451  volinun  25497  volfiniun  25498  volsup  25507  icombl  25515  ioombl  25516  ovolioo  25519  ioorcl2  25523  volivth  25558  ismbf3d  25605  dvferm2lem  25940  lhop  25971  tayl0  26319  pserulm  26381  cxpcn3  26708  ssscongptld  26782  heron  26798  mpodvdsmulf1o  27154  dvdsmulf1o  27156  logexprlim  27186  perfectlem2  27191  lgssq  27298  lgssq2  27299  gausslemma2dlem7  27334  lgsquad2lem1  27345  lgsquad2lem2  27346  2sqblem  27392  addsq2nreurex  27405  ostth2lem2  27595  ostth3  27599  ubthlem2  30798  nmopleid  32066  elsuppfnd  32605  fsuppcurry1  32648  fsuppcurry2  32649  znumd  32737  zdend  32738  numdenneg  32739  mgcf1olem1  32927  mgcf1olem2  32928  gsummptres2  32993  archirngz  33133  archiabllem1a  33135  elrgspnlem2  33184  elrgspnlem3  33185  q1pdir  33558  q1pvsca  33559  ply1degltdimlem  33608  fedgmullem1  33615  fedgmullem2  33616  evls1fldgencl  33657  cos9thpiminplylem1  33762  cos9thpiminplylem2  33763  submatminr1  33787  locfinreflem  33817  sxbrsigalem2  34264  elmrsubrn  35488  ismblfin  37631  itg2gt0cn  37645  cntotbnd  37766  ismtyhmeolem  37774  heibor1lem  37779  heiborlem6  37786  rrnequiv  37805  1cvrat  39441  ps-2b  39447  2at0mat0  39490  ps-2c  39493  llncvrlpln2  39522  2llnmeqat  39536  4atlem10  39571  4atlem11a  39572  4atlem12a  39575  2lplnja  39584  dalemcea  39625  dalem2  39626  dalem21  39659  dalem54  39691  2lnat  39749  cdlemb  39759  elpaddat  39769  paddasslem7  39791  paddasslem9  39793  paddasslem10  39794  paddasslem15  39799  poml6N  39920  osumcllem6N  39926  osumcllem7N  39927  pexmidlem4N  39938  pl42lem4N  39947  lhplt  39965  lhpjat1  39985  cdlemc5  40160  cdlemeg46fgN  40499  cdlemg12g  40614  tendoco2  40733  tendococl  40737  tendodi1  40749  tendoicl  40761  cdlemi2  40784  tendospdi1  40985  dihord11c  41189  dihmeetlem6  41274  dihjatc1  41276  dihmeetlem10N  41281  fltnltalem  42632  jm2.20nn  42968  kercvrlsm  43054  omord2lim  43271  frege96d  43720  frege98d  43724  ntrclsk3  44041  snunioo1  45489  limcleqr  45621  dvdivbd  45900  volioc  45949  iblspltprt  45950  volico  45960  stoweidlem1  45978  stoweidlem24  46001  etransclem23  46234  submodlt  47327  iccpartipre  47383  2pwp1prm  47551  perfectALTVlem2  47684  lincresunit2  48402  expnegico01  48442  itscnhlinecirc02plem3  48712