Theorem syl32anc 1405

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 1400	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  9375  coftr  10352  fin1a2s  10493  ioounsn  13609  snunioo  13610  snunico  13611  snunioc  13612  leexp1ad  14320  exple1  14321  leexp2rd  14400  facubnd  14445  permnn  14471  sqgcd  16737  expgcd  16738  cncongr2  16844  prmdvdsbc  16903  hashgcdlem  16966  ramlb  17198  0ram  17199  ram0  17201  ramz2  17203  ramz  17204  ramcl  17208  lsmub1x  19861  lsmub2x  19862  lsmsubm  19868  pgpfac1lem2  20292  mptscmfsupp0  21203  2idlcpblrng  21566  xrsdsreclblem  21720  pzriprnglem12  21799  uvcff  22098  uvcresum  22100  frlmup1  22105  psrass1lem  22242  psrlidm  22270  psrridm  22271  psrcom  22276  mvrcl  22300  mplsubrglem  22312  mplcoe5  22350  mplbas2  22352  psrbagev1  22387  evlslem3  22390  evlslem6  22391  psropprmul  22556  evls1fpws  22688  smadiadetg  22989  cayhamlem4  23207  lecldbas  23538  pnfnei  23539  mnfnei  23540  clsconn  23749  txcls  23924  ufldom  24282  hauspwpwf1  24307  flfcnp  24324  flfcnp2  24327  cnpfcfi  24360  tsmsmhm  24466  met2ndci  24842  nghmco  25058  nghmplusg  25060  icopnfcld  25087  iocmnfcld  25088  tgioo  25116  reconnlem1  25147  metdseq0  25175  ovolunnul  25822  volinun  25868  volfiniun  25869  volsup  25878  icombl  25886  ioombl  25887  ovolioo  25890  ioorcl2  25894  volivth  25929  ismbf3d  25976  dvferm2lem  26307  lhop  26337  tayl0  26690  pserulm  26750  cxpcn3  27077  ssscongptld  27151  heron  27167  mpodvdsmulf1o  27522  dvdsmulf1o  27524  logexprlim  27553  perfectlem2  27558  lgssq  27665  lgssq2  27666  gausslemma2dlem7  27701  lgsquad2lem1  27712  lgsquad2lem2  27713  2sqblem  27759  addsq2nreurex  27772  ostth2lem2  27962  ostth3  27966  bdayfinbndlem1  28854  ubthlem2  31474  nmopleid  32742  elsuppfnd  33318  fsuppcurry1  33359  fsuppcurry2  33360  znumd  33447  zdend  33448  numdenneg  33449  mgcf1olem1  33605  mgcf1olem2  33606  gsummptres2  33657  archirngz  33793  archiabllem1a  33795  elrgspnlem2  33847  elrgspnlem3  33848  q1pdir  34178  q1pvsca  34179  ply1degltdimlem  34297  fedgmullem1  34304  fedgmullem2  34305  evls1fldgencl  34345  cos9thpiminplylem1  34457  cos9thpiminplylem2  34458  submatminr1  34485  locfinreflem  34515  sxbrsigalem2  34961  elmrsubrn  36354  ismblfin  38655  itg2gt0cn  38669  cntotbnd  38806  ismtyhmeolem  38814  heibor1lem  38819  heiborlem6  38826  rrnequiv  38845  1cvrat  40609  ps-2b  40615  2at0mat0  40658  ps-2c  40661  llncvrlpln2  40690  2llnmeqat  40704  4atlem10  40739  4atlem11a  40740  4atlem12a  40743  2lplnja  40752  dalemcea  40793  dalem2  40794  dalem21  40827  dalem54  40859  2lnat  40917  cdlemb  40927  elpaddat  40937  paddasslem7  40959  paddasslem9  40961  paddasslem10  40962  paddasslem15  40967  poml6N  41088  osumcllem6N  41094  osumcllem7N  41095  pexmidlem4N  41106  pl42lem4N  41115  lhplt  41133  lhpjat1  41153  cdlemc5  41328  cdlemeg46fgN  41667  cdlemg12g  41782  tendoco2  41901  tendococl  41905  tendodi1  41917  tendoicl  41929  cdlemi2  41952  tendospdi1  42153  dihord11c  42357  dihmeetlem6  42442  dihjatc1  42444  dihmeetlem10N  42449  fltnltalem  43749  jm2.20nn  44080  kercvrlsm  44161  omord2lim  44378  frege96d  44825  frege98d  44829  ntrclsk3  45146  snunioo1  46600  limcleqr  46730  dvdivbd  47009  volioc  47058  iblspltprt  47059  volico  47069  stoweidlem1  47087  stoweidlem24  47110  etransclem23  47343  submodlt  48502  iccpartipre  48579  2pwp1prm  48750  perfectALTVlem2  48896  lincresunit2  49666  expnegico01  49706  itscnhlinecirc02plem3  49972