Theorem syl32anc 1334

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl12anc.1	⊢ (𝜑 → 𝜓)
syl12anc.2	⊢ (𝜑 → 𝜒)
syl12anc.3	⊢ (𝜑 → 𝜃)
syl22anc.4	⊢ (𝜑 → 𝜏)
syl23anc.5	⊢ (𝜑 → 𝜂)
syl32anc.6	⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁)

Assertion

Ref	Expression
syl32anc	⊢ (𝜑 → 𝜁)

Proof of Theorem syl32anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl12anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl12anc.3	. 2 ⊢ (𝜑 → 𝜃)
4		syl22anc.4	. . 3 ⊢ (𝜑 → 𝜏)
5		syl23anc.5	. . 3 ⊢ (𝜑 → 𝜂)
6	4, 5	jca 554	. 2 ⊢ (𝜑 → (𝜏 ∧ 𝜂))
7		syl32anc.6	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁)
8	1, 2, 3, 6, 7	syl31anc 1329	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  coftr  9095  fin1a2s  9236  snunioo  12298  snunico  12299  snunioc  12300  exple1  12920  leexp2rd  13042  facubnd  13087  permnn  13113  reuccats1  13480  dvdsadd2b  15028  dvdsmulgcd  15274  sqgcd  15278  bezoutr  15281  cncongr2  15382  hashgcdlem  15493  ramlb  15723  0ram  15724  ram0  15726  ramz2  15728  ramz  15729  ramcl  15733  lsmub1x  18061  lsmub2x  18062  lsmsubm  18068  pgpfac1lem2  18474  mptscmfsupp0  18928  psrass1lem  19377  psrlidm  19403  psrridm  19404  psrcom  19409  mplsubrglem  19439  mvrcl  19449  mplcoe5  19468  mplbas2  19470  psrbagev1  19510  evlslem6  19513  evlslem3  19514  psropprmul  19608  xrsdsreclblem  19792  uvcff  20130  uvcresum  20132  frlmup1  20137  smadiadetg  20479  cayhamlem4  20693  lecldbas  21023  pnfnei  21024  mnfnei  21025  clsconn  21233  txcls  21407  ufldom  21766  hauspwpwf1  21791  flfcnp  21808  flfcnp2  21811  cnpfcfi  21844  tsmsmhm  21949  met2ndci  22327  nghmco  22542  nghmplusg  22544  icopnfcld  22571  iocmnfcld  22572  tgioo  22599  reconnlem1  22629  metdseq0  22657  ovolunnul  23268  volinun  23314  volfiniun  23315  volsup  23324  icombl  23332  ioombl  23333  ovolioo  23336  ioorcl2  23340  volivth  23375  ismbf3d  23421  dvferm2lem  23749  lhop  23779  tayl0  24116  pserulm  24176  cxpcn3  24489  ssscongptld  24552  heron  24565  dvdsmulf1o  24920  logexprlim  24950  perfectlem2  24955  lgssq  25062  lgssq2  25063  gausslemma2dlem7  25098  lgsquad2lem1  25109  lgsquad2lem2  25110  2sqblem  25156  ostth2lem2  25323  ostth3  25327  ubthlem2  27727  nmopleid  28998  numdenneg  29563  2sqcoprm  29647  archirngz  29743  archiabllem1a  29745  submatminr1  29876  locfinreflem  29907  sxbrsigalem2  30348  oddpwdc  30416  ballotlemsdom  30573  ballotlemsel1i  30574  ballotlemsima  30577  ballotlemfrcn0  30591  fsum2dsub  30685  circlemeth  30718  elmrsubrn  31417  ismblfin  33450  itg2gt0cn  33465  cntotbnd  33595  ismtyhmeolem  33603  heibor1lem  33608  heiborlem6  33615  rrnequiv  33634  1cvrat  34762  ps-2b  34768  2at0mat0  34811  ps-2c  34814  llncvrlpln2  34843  2llnmeqat  34857  4atlem10  34892  4atlem11a  34893  4atlem12a  34896  2lplnja  34905  dalemcea  34946  dalem2  34947  dalem21  34980  dalem54  35012  2lnat  35070  cdlemb  35080  elpaddat  35090  paddasslem7  35112  paddasslem9  35114  paddasslem10  35115  paddasslem15  35120  poml6N  35241  osumcllem6N  35247  osumcllem7N  35248  pexmidlem4N  35259  pl42lem4N  35268  lhplt  35286  lhpjat1  35306  cdlemc5  35482  cdlemeg46fgN  35822  cdlemg12g  35937  tendoco2  36056  tendococl  36060  tendodi1  36072  tendoicl  36084  cdlemi2  36107  tendospdi1  36309  dihord11c  36513  dihmeetlem6  36598  dihjatc1  36600  dihmeetlem10N  36605  jm2.20nn  37564  jm2.25  37566  kercvrlsm  37653  frege96d  38041  frege98d  38045  ntrclsk3  38368  binomcxplemnn0  38548  snunioo2  39731  snunioo1  39738  limcleqr  39876  dvdivbd  40138  volioc  40188  iblspltprt  40189  volico  40200  stoweidlem1  40218  stoweidlem20  40237  stoweidlem24  40241  etransclem23  40474  iccpartipre  41357  2pwp1prm  41503  perfectALTVlem2  41631  lincresunit2  42267  expnegico01  42308