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

Syntax hints:   → wi 4   ∧ wa 399   ∧ 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 210  df-an 400  df-3an 1086

This theorem is referenced by:  coftr  9684  fin1a2s  9825  ioounsn  12855  snunioo  12856  snunico  12857  snunioc  12858  exple1  13536  leexp2rd  13614  facubnd  13656  permnn  13682  dvdsadd2b  15648  dvdsmulgcd  15895  sqgcd  15899  bezoutr  15902  cncongr2  16002  hashgcdlem  16115  ramlb  16345  0ram  16346  ram0  16348  ramz2  16350  ramz  16351  ramcl  16355  lsmub1x  18763  lsmub2x  18764  lsmsubm  18770  pgpfac1lem2  19190  mptscmfsupp0  19692  xrsdsreclblem  20137  uvcff  20480  uvcresum  20482  frlmup1  20487  psrass1lem  20615  psrlidm  20641  psrridm  20642  psrcom  20647  mplsubrglem  20677  mvrcl  20688  mplcoe5  20708  mplbas2  20710  psrbagev1  20749  evlslem3  20752  evlslem6  20753  psropprmul  20867  smadiadetg  21278  cayhamlem4  21493  lecldbas  21824  pnfnei  21825  mnfnei  21826  clsconn  22035  txcls  22209  ufldom  22567  hauspwpwf1  22592  flfcnp  22609  flfcnp2  22612  cnpfcfi  22645  tsmsmhm  22751  met2ndci  23129  nghmco  23344  nghmplusg  23346  icopnfcld  23373  iocmnfcld  23374  tgioo  23401  reconnlem1  23431  metdseq0  23459  ovolunnul  24104  volinun  24150  volfiniun  24151  volsup  24160  icombl  24168  ioombl  24169  ovolioo  24172  ioorcl2  24176  volivth  24211  ismbf3d  24258  dvferm2lem  24589  lhop  24619  tayl0  24957  pserulm  25017  cxpcn3  25337  ssscongptld  25408  heron  25424  dvdsmulf1o  25779  logexprlim  25809  perfectlem2  25814  lgssq  25921  lgssq2  25922  gausslemma2dlem7  25957  lgsquad2lem1  25968  lgsquad2lem2  25969  2sqblem  26015  2sqcoprm  26019  addsq2nreurex  26028  ostth2lem2  26218  ostth3  26222  ubthlem2  28654  nmopleid  29922  fsuppcurry1  30487  fsuppcurry2  30488  prmdvdsbc  30558  numdenneg  30559  pfxlsw2ccat  30652  wrdt2ind  30653  gsummptres2  30738  cyc3conja  30849  archirngz  30868  archiabllem1a  30870  fedgmullem1  31113  fedgmullem2  31114  submatminr1  31163  locfinreflem  31193  sxbrsigalem2  31654  oddpwdc  31722  ballotlemsdom  31879  ballotlemsel1i  31880  ballotlemsima  31883  ballotlemfrcn0  31897  fsum2dsub  31988  circlemeth  32021  elmrsubrn  32880  ismblfin  35098  itg2gt0cn  35112  cntotbnd  35234  ismtyhmeolem  35242  heibor1lem  35247  heiborlem6  35254  rrnequiv  35273  1cvrat  36772  ps-2b  36778  2at0mat0  36821  ps-2c  36824  llncvrlpln2  36853  2llnmeqat  36867  4atlem10  36902  4atlem11a  36903  4atlem12a  36906  2lplnja  36915  dalemcea  36956  dalem2  36957  dalem21  36990  dalem54  37022  2lnat  37080  cdlemb  37090  elpaddat  37100  paddasslem7  37122  paddasslem9  37124  paddasslem10  37125  paddasslem15  37130  poml6N  37251  osumcllem6N  37257  osumcllem7N  37258  pexmidlem4N  37269  pl42lem4N  37278  lhplt  37296  lhpjat1  37316  cdlemc5  37491  cdlemeg46fgN  37830  cdlemg12g  37945  tendoco2  38064  tendococl  38068  tendodi1  38080  tendoicl  38092  cdlemi2  38115  tendospdi1  38316  dihord11c  38520  dihmeetlem6  38605  dihjatc1  38607  dihmeetlem10N  38612  prodsplit  39386  expgcd  39491  fltnltalem  39618  jm2.20nn  39938  jm2.25  39940  kercvrlsm  40027  frege96d  40450  frege98d  40454  ntrclsk3  40773  binomcxplemnn0  41053  snunioo1  42149  limcleqr  42286  dvdivbd  42565  volioc  42614  iblspltprt  42615  volico  42625  stoweidlem1  42643  stoweidlem20  42662  stoweidlem24  42666  etransclem23  42899  iccpartipre  43938  2pwp1prm  44106  perfectALTVlem2  44240  lincresunit2  44887  expnegico01  44927  itscnhlinecirc02plem3  45198