Theorem syl32anc 1375

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  fsuppsssuppgd  9415  coftr  10304  fin1a2s  10445  ioounsn  13499  snunioo  13500  snunico  13501  snunioc  13502  exple1  14186  leexp2rd  14264  facubnd  14309  permnn  14335  sqgcd  16555  expgcd  16556  cncongr2  16661  prmdvdsbc  16720  hashgcdlem  16782  ramlb  17013  0ram  17014  ram0  17016  ramz2  17018  ramz  17019  ramcl  17023  lsmub1x  19637  lsmub2x  19638  lsmsubm  19644  pgpfac1lem2  20068  mptscmfsupp0  20896  2idlcpblrng  21253  xrsdsreclblem  21402  pzriprnglem12  21475  uvcff  21782  uvcresum  21784  frlmup1  21789  psrass1lemOLD  21931  psrass1lem  21934  psrlidm  21964  psrridm  21965  psrcom  21970  mvrcl  21994  mplsubrglem  22006  mplcoe5  22040  mplbas2  22042  psrbagev1  22083  psrbagev1OLD  22084  evlslem3  22088  evlslem6  22089  psropprmul  22220  evls1fpws  22354  smadiadetg  22660  cayhamlem4  22875  lecldbas  23208  pnfnei  23209  mnfnei  23210  clsconn  23419  txcls  23593  ufldom  23951  hauspwpwf1  23976  flfcnp  23993  flfcnp2  23996  cnpfcfi  24029  tsmsmhm  24135  met2ndci  24516  nghmco  24740  nghmplusg  24742  icopnfcld  24769  iocmnfcld  24770  tgioo  24797  reconnlem1  24827  metdseq0  24855  ovolunnul  25514  volinun  25560  volfiniun  25561  volsup  25570  icombl  25578  ioombl  25579  ovolioo  25582  ioorcl2  25586  volivth  25621  ismbf3d  25668  dvferm2lem  26003  lhop  26034  tayl0  26383  pserulm  26445  cxpcn3  26770  ssscongptld  26844  heron  26860  mpodvdsmulf1o  27216  dvdsmulf1o  27218  logexprlim  27248  perfectlem2  27253  lgssq  27360  lgssq2  27361  gausslemma2dlem7  27396  lgsquad2lem1  27407  lgsquad2lem2  27408  2sqblem  27454  addsq2nreurex  27467  ostth2lem2  27657  ostth3  27661  ubthlem2  30798  nmopleid  32066  fsuppcurry1  32636  fsuppcurry2  32637  znumd  32713  zdend  32714  numdenneg  32715  mgcf1olem1  32871  mgcf1olem2  32872  gsummptres2  32922  archirngz  33055  archiabllem1a  33057  q1pdir  33473  q1pvsca  33474  ply1degltdimlem  33520  fedgmullem1  33527  fedgmullem2  33528  evls1fldgencl  33559  submatminr1  33635  locfinreflem  33665  sxbrsigalem2  34130  elmrsubrn  35358  ismblfin  37372  itg2gt0cn  37386  cntotbnd  37507  ismtyhmeolem  37515  heibor1lem  37520  heiborlem6  37527  rrnequiv  37546  1cvrat  39185  ps-2b  39191  2at0mat0  39234  ps-2c  39237  llncvrlpln2  39266  2llnmeqat  39280  4atlem10  39315  4atlem11a  39316  4atlem12a  39319  2lplnja  39328  dalemcea  39369  dalem2  39370  dalem21  39403  dalem54  39435  2lnat  39493  cdlemb  39503  elpaddat  39513  paddasslem7  39535  paddasslem9  39537  paddasslem10  39538  paddasslem15  39543  poml6N  39664  osumcllem6N  39670  osumcllem7N  39671  pexmidlem4N  39682  pl42lem4N  39691  lhplt  39709  lhpjat1  39729  cdlemc5  39904  cdlemeg46fgN  40243  cdlemg12g  40358  tendoco2  40477  tendococl  40481  tendodi1  40493  tendoicl  40505  cdlemi2  40528  tendospdi1  40729  dihord11c  40933  dihmeetlem6  41018  dihjatc1  41020  dihmeetlem10N  41025  fltnltalem  42349  jm2.20nn  42689  kercvrlsm  42778  omord2lim  43000  frege96d  43450  frege98d  43454  ntrclsk3  43771  snunioo1  45163  limcleqr  45298  dvdivbd  45577  volioc  45626  iblspltprt  45627  volico  45637  stoweidlem1  45655  stoweidlem24  45678  etransclem23  45911  iccpartipre  47026  2pwp1prm  47194  perfectALTVlem2  47327  lincresunit2  47894  expnegico01  47934  itscnhlinecirc02plem3  48205