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  9352  coftr  10323  fin1a2s  10464  ioounsn  13578  snunioo  13579  snunico  13580  snunioc  13581  leexp1ad  14288  exple1  14289  leexp2rd  14367  facubnd  14412  permnn  14438  sqgcd  16700  expgcd  16701  cncongr2  16806  prmdvdsbc  16865  hashgcdlem  16927  ramlb  17159  0ram  17160  ram0  17162  ramz2  17164  ramz  17165  ramcl  17169  lsmub1x  19822  lsmub2x  19823  lsmsubm  19829  pgpfac1lem2  20253  mptscmfsupp0  21164  2idlcpblrng  21527  xrsdsreclblem  21681  pzriprnglem12  21760  uvcff  22059  uvcresum  22061  frlmup1  22066  psrass1lem  22203  psrlidm  22231  psrridm  22232  psrcom  22237  mvrcl  22261  mplsubrglem  22273  mplcoe5  22311  mplbas2  22313  psrbagev1  22348  evlslem3  22351  evlslem6  22352  psropprmul  22517  evls1fpws  22649  smadiadetg  22950  cayhamlem4  23168  lecldbas  23499  pnfnei  23500  mnfnei  23501  clsconn  23710  txcls  23885  ufldom  24243  hauspwpwf1  24268  flfcnp  24285  flfcnp2  24288  cnpfcfi  24321  tsmsmhm  24427  met2ndci  24803  nghmco  25019  nghmplusg  25021  icopnfcld  25048  iocmnfcld  25049  tgioo  25077  reconnlem1  25108  metdseq0  25136  ovolunnul  25783  volinun  25829  volfiniun  25830  volsup  25839  icombl  25847  ioombl  25848  ovolioo  25851  ioorcl2  25855  volivth  25890  ismbf3d  25937  dvferm2lem  26268  lhop  26298  tayl0  26653  pserulm  26713  cxpcn3  27040  ssscongptld  27114  heron  27130  mpodvdsmulf1o  27485  dvdsmulf1o  27487  logexprlim  27516  perfectlem2  27521  lgssq  27628  lgssq2  27629  gausslemma2dlem7  27664  lgsquad2lem1  27675  lgsquad2lem2  27676  2sqblem  27722  addsq2nreurex  27735  ostth2lem2  27925  ostth3  27929  bdayfinbndlem1  28787  ubthlem2  31407  nmopleid  32675  elsuppfnd  33209  fsuppcurry1  33250  fsuppcurry2  33251  znumd  33338  zdend  33339  numdenneg  33340  mgcf1olem1  33496  mgcf1olem2  33497  gsummptres2  33548  archirngz  33684  archiabllem1a  33686  elrgspnlem2  33738  elrgspnlem3  33739  q1pdir  34069  q1pvsca  34070  ply1degltdimlem  34188  fedgmullem1  34195  fedgmullem2  34196  evls1fldgencl  34236  cos9thpiminplylem1  34348  cos9thpiminplylem2  34349  submatminr1  34376  locfinreflem  34406  sxbrsigalem2  34853  elmrsubrn  36206  ismblfin  38499  itg2gt0cn  38513  cntotbnd  38650  ismtyhmeolem  38658  heibor1lem  38663  heiborlem6  38670  rrnequiv  38689  1cvrat  40453  ps-2b  40459  2at0mat0  40502  ps-2c  40505  llncvrlpln2  40534  2llnmeqat  40548  4atlem10  40583  4atlem11a  40584  4atlem12a  40587  2lplnja  40596  dalemcea  40637  dalem2  40638  dalem21  40671  dalem54  40703  2lnat  40761  cdlemb  40771  elpaddat  40781  paddasslem7  40803  paddasslem9  40805  paddasslem10  40806  paddasslem15  40811  poml6N  40932  osumcllem6N  40938  osumcllem7N  40939  pexmidlem4N  40950  pl42lem4N  40959  lhplt  40977  lhpjat1  40997  cdlemc5  41172  cdlemeg46fgN  41511  cdlemg12g  41626  tendoco2  41745  tendococl  41749  tendodi1  41761  tendoicl  41773  cdlemi2  41796  tendospdi1  41997  dihord11c  42201  dihmeetlem6  42286  dihjatc1  42288  dihmeetlem10N  42293  fltnltalem  43612  jm2.20nn  43942  kercvrlsm  44028  omord2lim  44245  frege96d  44693  frege98d  44697  ntrclsk3  45014  snunioo1  46446  limcleqr  46576  dvdivbd  46855  volioc  46904  iblspltprt  46905  volico  46915  stoweidlem1  46933  stoweidlem24  46956  etransclem23  47189  submodlt  48348  iccpartipre  48425  2pwp1prm  48596  perfectALTVlem2  48742  lincresunit2  49512  expnegico01  49552  itscnhlinecirc02plem3  49818