Theorem syl32anc 1376

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 1371	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  coftr  9960  fin1a2s  10101  ioounsn  13138  snunioo  13139  snunico  13140  snunioc  13141  exple1  13822  leexp2rd  13900  facubnd  13942  permnn  13968  sqgcd  16198  cncongr2  16301  hashgcdlem  16417  ramlb  16648  0ram  16649  ram0  16651  ramz2  16653  ramz  16654  ramcl  16658  lsmub1x  19166  lsmub2x  19167  lsmsubm  19173  pgpfac1lem2  19593  mptscmfsupp0  20103  xrsdsreclblem  20556  uvcff  20908  uvcresum  20910  frlmup1  20915  psrass1lemOLD  21053  psrass1lem  21056  psrlidm  21082  psrridm  21083  psrcom  21088  mplsubrglem  21120  mvrcl  21131  mplcoe5  21151  mplbas2  21153  psrbagev1  21195  psrbagev1OLD  21196  evlslem3  21200  evlslem6  21201  psropprmul  21319  smadiadetg  21730  cayhamlem4  21945  lecldbas  22278  pnfnei  22279  mnfnei  22280  clsconn  22489  txcls  22663  ufldom  23021  hauspwpwf1  23046  flfcnp  23063  flfcnp2  23066  cnpfcfi  23099  tsmsmhm  23205  met2ndci  23584  nghmco  23808  nghmplusg  23810  icopnfcld  23837  iocmnfcld  23838  tgioo  23865  reconnlem1  23895  metdseq0  23923  ovolunnul  24569  volinun  24615  volfiniun  24616  volsup  24625  icombl  24633  ioombl  24634  ovolioo  24637  ioorcl2  24641  volivth  24676  ismbf3d  24723  dvferm2lem  25055  lhop  25085  tayl0  25426  pserulm  25486  cxpcn3  25806  ssscongptld  25877  heron  25893  dvdsmulf1o  26248  logexprlim  26278  perfectlem2  26283  lgssq  26390  lgssq2  26391  gausslemma2dlem7  26426  lgsquad2lem1  26437  lgsquad2lem2  26438  2sqblem  26484  addsq2nreurex  26497  ostth2lem2  26687  ostth3  26691  ubthlem2  29134  nmopleid  30402  fsuppcurry1  30962  fsuppcurry2  30963  prmdvdsbc  31032  numdenneg  31033  mgcf1olem1  31181  mgcf1olem2  31182  gsummptres2  31215  archirngz  31345  archiabllem1a  31347  fedgmullem1  31612  fedgmullem2  31613  submatminr1  31662  locfinreflem  31692  sxbrsigalem2  32153  elmrsubrn  33382  ismblfin  35745  itg2gt0cn  35759  cntotbnd  35881  ismtyhmeolem  35889  heibor1lem  35894  heiborlem6  35901  rrnequiv  35920  1cvrat  37417  ps-2b  37423  2at0mat0  37466  ps-2c  37469  llncvrlpln2  37498  2llnmeqat  37512  4atlem10  37547  4atlem11a  37548  4atlem12a  37551  2lplnja  37560  dalemcea  37601  dalem2  37602  dalem21  37635  dalem54  37667  2lnat  37725  cdlemb  37735  elpaddat  37745  paddasslem7  37767  paddasslem9  37769  paddasslem10  37770  paddasslem15  37775  poml6N  37896  osumcllem6N  37902  osumcllem7N  37903  pexmidlem4N  37914  pl42lem4N  37923  lhplt  37941  lhpjat1  37961  cdlemc5  38136  cdlemeg46fgN  38475  cdlemg12g  38590  tendoco2  38709  tendococl  38713  tendodi1  38725  tendoicl  38737  cdlemi2  38760  tendospdi1  38961  dihord11c  39165  dihmeetlem6  39250  dihjatc1  39252  dihmeetlem10N  39257  expgcd  40255  fltnltalem  40415  jm2.20nn  40735  kercvrlsm  40824  frege96d  41246  frege98d  41250  ntrclsk3  41569  snunioo1  42940  limcleqr  43075  dvdivbd  43354  volioc  43403  iblspltprt  43404  volico  43414  stoweidlem1  43432  stoweidlem24  43455  etransclem23  43688  iccpartipre  44761  2pwp1prm  44929  perfectALTVlem2  45062  lincresunit2  45707  expnegico01  45747  itscnhlinecirc02plem3  46018