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  9333  coftr  10226  fin1a2s  10367  ioounsn  13438  snunioo  13439  snunico  13440  snunioc  13441  leexp1ad  14141  exple1  14142  leexp2rd  14220  facubnd  14265  permnn  14291  sqgcd  16532  expgcd  16533  cncongr2  16638  prmdvdsbc  16696  hashgcdlem  16758  ramlb  16990  0ram  16991  ram0  16993  ramz2  16995  ramz  16996  ramcl  17000  lsmub1x  19576  lsmub2x  19577  lsmsubm  19583  pgpfac1lem2  20007  mptscmfsupp0  20833  2idlcpblrng  21181  xrsdsreclblem  21329  pzriprnglem12  21402  uvcff  21700  uvcresum  21702  frlmup1  21707  psrass1lem  21841  psrlidm  21871  psrridm  21872  psrcom  21877  mvrcl  21901  mplsubrglem  21913  mplcoe5  21947  mplbas2  21949  psrbagev1  21984  evlslem3  21987  evlslem6  21988  psropprmul  22122  evls1fpws  22256  smadiadetg  22560  cayhamlem4  22775  lecldbas  23106  pnfnei  23107  mnfnei  23108  clsconn  23317  txcls  23491  ufldom  23849  hauspwpwf1  23874  flfcnp  23891  flfcnp2  23894  cnpfcfi  23927  tsmsmhm  24033  met2ndci  24410  nghmco  24626  nghmplusg  24628  icopnfcld  24655  iocmnfcld  24656  tgioo  24684  reconnlem1  24715  metdseq0  24743  ovolunnul  25401  volinun  25447  volfiniun  25448  volsup  25457  icombl  25465  ioombl  25466  ovolioo  25469  ioorcl2  25473  volivth  25508  ismbf3d  25555  dvferm2lem  25890  lhop  25921  tayl0  26269  pserulm  26331  cxpcn3  26658  ssscongptld  26732  heron  26748  mpodvdsmulf1o  27104  dvdsmulf1o  27106  logexprlim  27136  perfectlem2  27141  lgssq  27248  lgssq2  27249  gausslemma2dlem7  27284  lgsquad2lem1  27295  lgsquad2lem2  27296  2sqblem  27342  addsq2nreurex  27355  ostth2lem2  27545  ostth3  27549  ubthlem2  30800  nmopleid  32068  elsuppfnd  32605  fsuppcurry1  32648  fsuppcurry2  32649  znumd  32737  zdend  32738  numdenneg  32739  mgcf1olem1  32927  mgcf1olem2  32928  gsummptres2  32993  archirngz  33143  archiabllem1a  33145  elrgspnlem2  33194  elrgspnlem3  33195  q1pdir  33568  q1pvsca  33569  ply1degltdimlem  33618  fedgmullem1  33625  fedgmullem2  33626  evls1fldgencl  33665  cos9thpiminplylem1  33772  cos9thpiminplylem2  33773  submatminr1  33800  locfinreflem  33830  sxbrsigalem2  34277  elmrsubrn  35507  ismblfin  37655  itg2gt0cn  37669  cntotbnd  37790  ismtyhmeolem  37798  heibor1lem  37803  heiborlem6  37810  rrnequiv  37829  1cvrat  39470  ps-2b  39476  2at0mat0  39519  ps-2c  39522  llncvrlpln2  39551  2llnmeqat  39565  4atlem10  39600  4atlem11a  39601  4atlem12a  39604  2lplnja  39613  dalemcea  39654  dalem2  39655  dalem21  39688  dalem54  39720  2lnat  39778  cdlemb  39788  elpaddat  39798  paddasslem7  39820  paddasslem9  39822  paddasslem10  39823  paddasslem15  39828  poml6N  39949  osumcllem6N  39955  osumcllem7N  39956  pexmidlem4N  39967  pl42lem4N  39976  lhplt  39994  lhpjat1  40014  cdlemc5  40189  cdlemeg46fgN  40528  cdlemg12g  40643  tendoco2  40762  tendococl  40766  tendodi1  40778  tendoicl  40790  cdlemi2  40813  tendospdi1  41014  dihord11c  41218  dihmeetlem6  41303  dihjatc1  41305  dihmeetlem10N  41310  fltnltalem  42650  jm2.20nn  42986  kercvrlsm  43072  omord2lim  43289  frege96d  43738  frege98d  43742  ntrclsk3  44059  snunioo1  45510  limcleqr  45642  dvdivbd  45921  volioc  45970  iblspltprt  45971  volico  45981  stoweidlem1  45999  stoweidlem24  46022  etransclem23  46255  submodlt  47351  iccpartipre  47422  2pwp1prm  47590  perfectALTVlem2  47723  lincresunit2  48467  expnegico01  48507  itscnhlinecirc02plem3  48773