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  9261  coftr  10156  fin1a2s  10297  ioounsn  13369  snunioo  13370  snunico  13371  snunioc  13372  leexp1ad  14075  exple1  14076  leexp2rd  14154  facubnd  14199  permnn  14225  sqgcd  16465  expgcd  16466  cncongr2  16571  prmdvdsbc  16629  hashgcdlem  16691  ramlb  16923  0ram  16924  ram0  16926  ramz2  16928  ramz  16929  ramcl  16933  lsmub1x  19551  lsmub2x  19552  lsmsubm  19558  pgpfac1lem2  19982  mptscmfsupp0  20853  2idlcpblrng  21201  xrsdsreclblem  21342  pzriprnglem12  21422  uvcff  21721  uvcresum  21723  frlmup1  21728  psrass1lem  21862  psrlidm  21892  psrridm  21893  psrcom  21898  mvrcl  21922  mplsubrglem  21934  mplcoe5  21968  mplbas2  21970  psrbagev1  22005  evlslem3  22008  evlslem6  22009  psropprmul  22143  evls1fpws  22277  smadiadetg  22581  cayhamlem4  22796  lecldbas  23127  pnfnei  23128  mnfnei  23129  clsconn  23338  txcls  23512  ufldom  23870  hauspwpwf1  23895  flfcnp  23912  flfcnp2  23915  cnpfcfi  23948  tsmsmhm  24054  met2ndci  24430  nghmco  24646  nghmplusg  24648  icopnfcld  24675  iocmnfcld  24676  tgioo  24704  reconnlem1  24735  metdseq0  24763  ovolunnul  25421  volinun  25467  volfiniun  25468  volsup  25477  icombl  25485  ioombl  25486  ovolioo  25489  ioorcl2  25493  volivth  25528  ismbf3d  25575  dvferm2lem  25910  lhop  25941  tayl0  26289  pserulm  26351  cxpcn3  26678  ssscongptld  26752  heron  26768  mpodvdsmulf1o  27124  dvdsmulf1o  27126  logexprlim  27156  perfectlem2  27161  lgssq  27268  lgssq2  27269  gausslemma2dlem7  27304  lgsquad2lem1  27315  lgsquad2lem2  27316  2sqblem  27362  addsq2nreurex  27375  ostth2lem2  27565  ostth3  27569  ubthlem2  30841  nmopleid  32109  elsuppfnd  32653  fsuppcurry1  32697  fsuppcurry2  32698  znumd  32785  zdend  32786  numdenneg  32787  mgcf1olem1  32972  mgcf1olem2  32973  gsummptres2  33023  archirngz  33148  archiabllem1a  33150  elrgspnlem2  33200  elrgspnlem3  33201  q1pdir  33553  q1pvsca  33554  ply1degltdimlem  33625  fedgmullem1  33632  fedgmullem2  33633  evls1fldgencl  33673  cos9thpiminplylem1  33785  cos9thpiminplylem2  33786  submatminr1  33813  locfinreflem  33843  sxbrsigalem2  34289  elmrsubrn  35532  ismblfin  37680  itg2gt0cn  37694  cntotbnd  37815  ismtyhmeolem  37823  heibor1lem  37828  heiborlem6  37835  rrnequiv  37854  1cvrat  39494  ps-2b  39500  2at0mat0  39543  ps-2c  39546  llncvrlpln2  39575  2llnmeqat  39589  4atlem10  39624  4atlem11a  39625  4atlem12a  39628  2lplnja  39637  dalemcea  39678  dalem2  39679  dalem21  39712  dalem54  39744  2lnat  39802  cdlemb  39812  elpaddat  39822  paddasslem7  39844  paddasslem9  39846  paddasslem10  39847  paddasslem15  39852  poml6N  39973  osumcllem6N  39979  osumcllem7N  39980  pexmidlem4N  39991  pl42lem4N  40000  lhplt  40018  lhpjat1  40038  cdlemc5  40213  cdlemeg46fgN  40552  cdlemg12g  40667  tendoco2  40786  tendococl  40790  tendodi1  40802  tendoicl  40814  cdlemi2  40837  tendospdi1  41038  dihord11c  41242  dihmeetlem6  41327  dihjatc1  41329  dihmeetlem10N  41334  fltnltalem  42674  jm2.20nn  43009  kercvrlsm  43095  omord2lim  43312  frege96d  43761  frege98d  43765  ntrclsk3  44082  snunioo1  45531  limcleqr  45661  dvdivbd  45940  volioc  45989  iblspltprt  45990  volico  46000  stoweidlem1  46018  stoweidlem24  46041  etransclem23  46274  submodlt  47360  iccpartipre  47431  2pwp1prm  47599  perfectALTVlem2  47732  lincresunit2  48489  expnegico01  48529  itscnhlinecirc02plem3  48795