Theorem syl32anc 1404

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∧ w3a 1102

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 401  df-3an 1104

This theorem is used by:  fsuppsssuppgd  9340  coftr  10263  fin1a2s  10404  ioounsn  13510  snunioo  13511  snunico  13512  snunioc  13513  leexp1ad  14219  exple1  14220  leexp2rd  14298  facubnd  14343  permnn  14369  sqgcd  16626  expgcd  16627  cncongr2  16732  prmdvdsbc  16791  hashgcdlem  16853  ramlb  17085  0ram  17086  ram0  17088  ramz2  17090  ramz  17091  ramcl  17095  lsmub1x  19722  lsmub2x  19723  lsmsubm  19729  pgpfac1lem2  20153  mptscmfsupp0  21059  2idlcpblrng  21421  xrsdsreclblem  21574  pzriprnglem12  21653  uvcff  21952  uvcresum  21954  frlmup1  21959  psrass1lem  22094  psrlidm  22122  psrridm  22123  psrcom  22128  mvrcl  22152  mplsubrglem  22164  mplcoe5  22202  mplbas2  22204  psrbagev1  22239  evlslem3  22242  evlslem6  22243  psropprmul  22408  evls1fpws  22540  smadiadetg  22841  cayhamlem4  23056  lecldbas  23387  pnfnei  23388  mnfnei  23389  clsconn  23598  txcls  23772  ufldom  24130  hauspwpwf1  24155  flfcnp  24172  flfcnp2  24175  cnpfcfi  24208  tsmsmhm  24314  met2ndci  24690  nghmco  24906  nghmplusg  24908  icopnfcld  24935  iocmnfcld  24936  tgioo  24964  reconnlem1  24995  metdseq0  25023  ovolunnul  25670  volinun  25716  volfiniun  25717  volsup  25726  icombl  25734  ioombl  25735  ovolioo  25738  ioorcl2  25742  volivth  25777  ismbf3d  25824  dvferm2lem  26156  lhop  26186  tayl0  26536  pserulm  26596  cxpcn3  26924  ssscongptld  26998  heron  27014  mpodvdsmulf1o  27369  dvdsmulf1o  27371  logexprlim  27400  perfectlem2  27405  lgssq  27512  lgssq2  27513  gausslemma2dlem7  27548  lgsquad2lem1  27559  lgsquad2lem2  27560  2sqblem  27606  addsq2nreurex  27619  ostth2lem2  27809  ostth3  27813  bdayfinbndlem1  28671  ubthlem2  31234  nmopleid  32502  elsuppfnd  33038  fsuppcurry1  33080  fsuppcurry2  33081  znumd  33168  zdend  33169  numdenneg  33170  mgcf1olem1  33330  mgcf1olem2  33331  gsummptres2  33382  archirngz  33518  archiabllem1a  33520  elrgspnlem2  33572  elrgspnlem3  33573  q1pdir  33902  q1pvsca  33903  ply1degltdimlem  34021  fedgmullem1  34028  fedgmullem2  34029  evls1fldgencl  34069  cos9thpiminplylem1  34181  cos9thpiminplylem2  34182  submatminr1  34209  locfinreflem  34239  sxbrsigalem2  34685  elmrsubrn  36020  ismblfin  38340  itg2gt0cn  38354  cntotbnd  38475  ismtyhmeolem  38483  heibor1lem  38488  heiborlem6  38495  rrnequiv  38514  1cvrat  40278  ps-2b  40284  2at0mat0  40327  ps-2c  40330  llncvrlpln2  40359  2llnmeqat  40373  4atlem10  40408  4atlem11a  40409  4atlem12a  40412  2lplnja  40421  dalemcea  40462  dalem2  40463  dalem21  40496  dalem54  40528  2lnat  40586  cdlemb  40596  elpaddat  40606  paddasslem7  40628  paddasslem9  40630  paddasslem10  40631  paddasslem15  40636  poml6N  40757  osumcllem6N  40763  osumcllem7N  40764  pexmidlem4N  40775  pl42lem4N  40784  lhplt  40802  lhpjat1  40822  cdlemc5  40997  cdlemeg46fgN  41336  cdlemg12g  41451  tendoco2  41570  tendococl  41574  tendodi1  41586  tendoicl  41598  cdlemi2  41621  tendospdi1  41822  dihord11c  42026  dihmeetlem6  42111  dihjatc1  42113  dihmeetlem10N  42118  fltnltalem  43422  jm2.20nn  43752  kercvrlsm  43838  omord2lim  44055  frege96d  44503  frege98d  44507  ntrclsk3  44824  snunioo1  46256  limcleqr  46386  dvdivbd  46665  volioc  46714  iblspltprt  46715  volico  46725  stoweidlem1  46743  stoweidlem24  46766  etransclem23  46999  submodlt  48121  iccpartipre  48198  2pwp1prm  48369  perfectALTVlem2  48515  lincresunit2  49286  expnegico01  49326  itscnhlinecirc02plem3  49592