Theorem syl32anc 1381

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 1376	1 ⊢ (𝜑 → 𝜁)

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

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 1089

This theorem is referenced by:  fsuppsssuppgd  9286  coftr  10184  fin1a2s  10325  ioounsn  13419  snunioo  13420  snunico  13421  snunioc  13422  leexp1ad  14127  exple1  14128  leexp2rd  14206  facubnd  14251  permnn  14277  sqgcd  16520  expgcd  16521  cncongr2  16626  prmdvdsbc  16685  hashgcdlem  16747  ramlb  16979  0ram  16980  ram0  16982  ramz2  16984  ramz  16985  ramcl  16989  lsmub1x  19610  lsmub2x  19611  lsmsubm  19617  pgpfac1lem2  20041  mptscmfsupp0  20911  2idlcpblrng  21259  xrsdsreclblem  21400  pzriprnglem12  21480  uvcff  21779  uvcresum  21781  frlmup1  21786  psrass1lem  21920  psrlidm  21949  psrridm  21950  psrcom  21955  mvrcl  21979  mplsubrglem  21991  mplcoe5  22027  mplbas2  22029  psrbagev1  22064  evlslem3  22067  evlslem6  22068  psropprmul  22210  evls1fpws  22343  smadiadetg  22647  cayhamlem4  22862  lecldbas  23193  pnfnei  23194  mnfnei  23195  clsconn  23404  txcls  23578  ufldom  23936  hauspwpwf1  23961  flfcnp  23978  flfcnp2  23981  cnpfcfi  24014  tsmsmhm  24120  met2ndci  24496  nghmco  24712  nghmplusg  24714  icopnfcld  24741  iocmnfcld  24742  tgioo  24770  reconnlem1  24801  metdseq0  24829  ovolunnul  25476  volinun  25522  volfiniun  25523  volsup  25532  icombl  25540  ioombl  25541  ovolioo  25544  ioorcl2  25548  volivth  25583  ismbf3d  25630  dvferm2lem  25962  lhop  25993  tayl0  26340  pserulm  26402  cxpcn3  26729  ssscongptld  26803  heron  26819  mpodvdsmulf1o  27175  dvdsmulf1o  27177  logexprlim  27207  perfectlem2  27212  lgssq  27319  lgssq2  27320  gausslemma2dlem7  27355  lgsquad2lem1  27366  lgsquad2lem2  27367  2sqblem  27413  addsq2nreurex  27426  ostth2lem2  27616  ostth3  27620  bdayfinbndlem1  28478  ubthlem2  30962  nmopleid  32230  elsuppfnd  32775  fsuppcurry1  32817  fsuppcurry2  32818  znumd  32906  zdend  32907  numdenneg  32908  mgcf1olem1  33081  mgcf1olem2  33082  gsummptres2  33134  archirngz  33270  archiabllem1a  33272  elrgspnlem2  33324  elrgspnlem3  33325  q1pdir  33683  q1pvsca  33684  ply1degltdimlem  33787  fedgmullem1  33794  fedgmullem2  33795  evls1fldgencl  33835  cos9thpiminplylem1  33947  cos9thpiminplylem2  33948  submatminr1  33975  locfinreflem  34005  sxbrsigalem2  34451  elmrsubrn  35723  ismblfin  37993  itg2gt0cn  38007  cntotbnd  38128  ismtyhmeolem  38136  heibor1lem  38141  heiborlem6  38148  rrnequiv  38167  1cvrat  39933  ps-2b  39939  2at0mat0  39982  ps-2c  39985  llncvrlpln2  40014  2llnmeqat  40028  4atlem10  40063  4atlem11a  40064  4atlem12a  40067  2lplnja  40076  dalemcea  40117  dalem2  40118  dalem21  40151  dalem54  40183  2lnat  40241  cdlemb  40251  elpaddat  40261  paddasslem7  40283  paddasslem9  40285  paddasslem10  40286  paddasslem15  40291  poml6N  40412  osumcllem6N  40418  osumcllem7N  40419  pexmidlem4N  40430  pl42lem4N  40439  lhplt  40457  lhpjat1  40477  cdlemc5  40652  cdlemeg46fgN  40991  cdlemg12g  41106  tendoco2  41225  tendococl  41229  tendodi1  41241  tendoicl  41253  cdlemi2  41276  tendospdi1  41477  dihord11c  41681  dihmeetlem6  41766  dihjatc1  41768  dihmeetlem10N  41773  fltnltalem  43106  jm2.20nn  43440  kercvrlsm  43526  omord2lim  43743  frege96d  44191  frege98d  44195  ntrclsk3  44512  snunioo1  45957  limcleqr  46087  dvdivbd  46366  volioc  46415  iblspltprt  46416  volico  46426  stoweidlem1  46444  stoweidlem24  46467  etransclem23  46700  submodlt  47801  iccpartipre  47878  2pwp1prm  48049  perfectALTVlem2  48195  lincresunit2  48951  expnegico01  48991  itscnhlinecirc02plem3  49257