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  9273  coftr  10171  fin1a2s  10312  ioounsn  13379  snunioo  13380  snunico  13381  snunioc  13382  leexp1ad  14085  exple1  14086  leexp2rd  14164  facubnd  14209  permnn  14235  sqgcd  16475  expgcd  16476  cncongr2  16581  prmdvdsbc  16639  hashgcdlem  16701  ramlb  16933  0ram  16934  ram0  16936  ramz2  16938  ramz  16939  ramcl  16943  lsmub1x  19560  lsmub2x  19561  lsmsubm  19567  pgpfac1lem2  19991  mptscmfsupp0  20862  2idlcpblrng  21210  xrsdsreclblem  21351  pzriprnglem12  21431  uvcff  21730  uvcresum  21732  frlmup1  21737  psrass1lem  21871  psrlidm  21900  psrridm  21901  psrcom  21906  mvrcl  21930  mplsubrglem  21942  mplcoe5  21976  mplbas2  21978  psrbagev1  22013  evlslem3  22016  evlslem6  22017  psropprmul  22151  evls1fpws  22285  smadiadetg  22589  cayhamlem4  22804  lecldbas  23135  pnfnei  23136  mnfnei  23137  clsconn  23346  txcls  23520  ufldom  23878  hauspwpwf1  23903  flfcnp  23920  flfcnp2  23923  cnpfcfi  23956  tsmsmhm  24062  met2ndci  24438  nghmco  24654  nghmplusg  24656  icopnfcld  24683  iocmnfcld  24684  tgioo  24712  reconnlem1  24743  metdseq0  24771  ovolunnul  25429  volinun  25475  volfiniun  25476  volsup  25485  icombl  25493  ioombl  25494  ovolioo  25497  ioorcl2  25501  volivth  25536  ismbf3d  25583  dvferm2lem  25918  lhop  25949  tayl0  26297  pserulm  26359  cxpcn3  26686  ssscongptld  26760  heron  26776  mpodvdsmulf1o  27132  dvdsmulf1o  27134  logexprlim  27164  perfectlem2  27169  lgssq  27276  lgssq2  27277  gausslemma2dlem7  27312  lgsquad2lem1  27323  lgsquad2lem2  27324  2sqblem  27370  addsq2nreurex  27383  ostth2lem2  27573  ostth3  27577  ubthlem2  30853  nmopleid  32121  elsuppfnd  32667  fsuppcurry1  32711  fsuppcurry2  32712  znumd  32800  zdend  32801  numdenneg  32802  mgcf1olem1  32989  mgcf1olem2  32990  gsummptres2  33040  archirngz  33165  archiabllem1a  33167  elrgspnlem2  33217  elrgspnlem3  33218  q1pdir  33570  q1pvsca  33571  ply1degltdimlem  33656  fedgmullem1  33663  fedgmullem2  33664  evls1fldgencl  33704  cos9thpiminplylem1  33816  cos9thpiminplylem2  33817  submatminr1  33844  locfinreflem  33874  sxbrsigalem2  34320  elmrsubrn  35585  ismblfin  37721  itg2gt0cn  37735  cntotbnd  37856  ismtyhmeolem  37864  heibor1lem  37869  heiborlem6  37876  rrnequiv  37895  1cvrat  39595  ps-2b  39601  2at0mat0  39644  ps-2c  39647  llncvrlpln2  39676  2llnmeqat  39690  4atlem10  39725  4atlem11a  39726  4atlem12a  39729  2lplnja  39738  dalemcea  39779  dalem2  39780  dalem21  39813  dalem54  39845  2lnat  39903  cdlemb  39913  elpaddat  39923  paddasslem7  39945  paddasslem9  39947  paddasslem10  39948  paddasslem15  39953  poml6N  40074  osumcllem6N  40080  osumcllem7N  40081  pexmidlem4N  40092  pl42lem4N  40101  lhplt  40119  lhpjat1  40139  cdlemc5  40314  cdlemeg46fgN  40653  cdlemg12g  40768  tendoco2  40887  tendococl  40891  tendodi1  40903  tendoicl  40915  cdlemi2  40938  tendospdi1  41139  dihord11c  41343  dihmeetlem6  41428  dihjatc1  41430  dihmeetlem10N  41435  fltnltalem  42780  jm2.20nn  43114  kercvrlsm  43200  omord2lim  43417  frege96d  43866  frege98d  43870  ntrclsk3  44187  snunioo1  45636  limcleqr  45766  dvdivbd  46045  volioc  46094  iblspltprt  46095  volico  46105  stoweidlem1  46123  stoweidlem24  46146  etransclem23  46379  submodlt  47474  iccpartipre  47545  2pwp1prm  47713  perfectALTVlem2  47846  lincresunit2  48603  expnegico01  48643  itscnhlinecirc02plem3  48909