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  9276  coftr  10174  fin1a2s  10315  ioounsn  13387  snunioo  13388  snunico  13389  snunioc  13390  leexp1ad  14093  exple1  14094  leexp2rd  14172  facubnd  14217  permnn  14243  sqgcd  16483  expgcd  16484  cncongr2  16589  prmdvdsbc  16647  hashgcdlem  16709  ramlb  16941  0ram  16942  ram0  16944  ramz2  16946  ramz  16947  ramcl  16951  lsmub1x  19568  lsmub2x  19569  lsmsubm  19575  pgpfac1lem2  19999  mptscmfsupp0  20870  2idlcpblrng  21218  xrsdsreclblem  21359  pzriprnglem12  21439  uvcff  21738  uvcresum  21740  frlmup1  21745  psrass1lem  21879  psrlidm  21909  psrridm  21910  psrcom  21915  mvrcl  21939  mplsubrglem  21951  mplcoe5  21985  mplbas2  21987  psrbagev1  22022  evlslem3  22025  evlslem6  22026  psropprmul  22160  evls1fpws  22294  smadiadetg  22598  cayhamlem4  22813  lecldbas  23144  pnfnei  23145  mnfnei  23146  clsconn  23355  txcls  23529  ufldom  23887  hauspwpwf1  23912  flfcnp  23929  flfcnp2  23932  cnpfcfi  23965  tsmsmhm  24071  met2ndci  24447  nghmco  24663  nghmplusg  24665  icopnfcld  24692  iocmnfcld  24693  tgioo  24721  reconnlem1  24752  metdseq0  24780  ovolunnul  25438  volinun  25484  volfiniun  25485  volsup  25494  icombl  25502  ioombl  25503  ovolioo  25506  ioorcl2  25510  volivth  25545  ismbf3d  25592  dvferm2lem  25927  lhop  25958  tayl0  26306  pserulm  26368  cxpcn3  26695  ssscongptld  26769  heron  26785  mpodvdsmulf1o  27141  dvdsmulf1o  27143  logexprlim  27173  perfectlem2  27178  lgssq  27285  lgssq2  27286  gausslemma2dlem7  27321  lgsquad2lem1  27332  lgsquad2lem2  27333  2sqblem  27379  addsq2nreurex  27392  ostth2lem2  27582  ostth3  27586  ubthlem2  30862  nmopleid  32130  elsuppfnd  32674  fsuppcurry1  32718  fsuppcurry2  32719  znumd  32806  zdend  32807  numdenneg  32808  mgcf1olem1  32993  mgcf1olem2  32994  gsummptres2  33044  archirngz  33169  archiabllem1a  33171  elrgspnlem2  33221  elrgspnlem3  33222  q1pdir  33574  q1pvsca  33575  ply1degltdimlem  33646  fedgmullem1  33653  fedgmullem2  33654  evls1fldgencl  33694  cos9thpiminplylem1  33806  cos9thpiminplylem2  33807  submatminr1  33834  locfinreflem  33864  sxbrsigalem2  34310  elmrsubrn  35575  ismblfin  37711  itg2gt0cn  37725  cntotbnd  37846  ismtyhmeolem  37854  heibor1lem  37859  heiborlem6  37866  rrnequiv  37885  1cvrat  39585  ps-2b  39591  2at0mat0  39634  ps-2c  39637  llncvrlpln2  39666  2llnmeqat  39680  4atlem10  39715  4atlem11a  39716  4atlem12a  39719  2lplnja  39728  dalemcea  39769  dalem2  39770  dalem21  39803  dalem54  39835  2lnat  39893  cdlemb  39903  elpaddat  39913  paddasslem7  39935  paddasslem9  39937  paddasslem10  39938  paddasslem15  39943  poml6N  40064  osumcllem6N  40070  osumcllem7N  40071  pexmidlem4N  40082  pl42lem4N  40091  lhplt  40109  lhpjat1  40129  cdlemc5  40304  cdlemeg46fgN  40643  cdlemg12g  40758  tendoco2  40877  tendococl  40881  tendodi1  40893  tendoicl  40905  cdlemi2  40928  tendospdi1  41129  dihord11c  41333  dihmeetlem6  41418  dihjatc1  41420  dihmeetlem10N  41425  fltnltalem  42770  jm2.20nn  43104  kercvrlsm  43190  omord2lim  43407  frege96d  43856  frege98d  43860  ntrclsk3  44177  snunioo1  45626  limcleqr  45756  dvdivbd  46035  volioc  46084  iblspltprt  46085  volico  46095  stoweidlem1  46113  stoweidlem24  46136  etransclem23  46369  submodlt  47464  iccpartipre  47535  2pwp1prm  47703  perfectALTVlem2  47836  lincresunit2  48593  expnegico01  48633  itscnhlinecirc02plem3  48899