Theorem syl32anc 1381

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

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

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 1089

This theorem is referenced by:  fsuppsssuppgd  9297  coftr  10195  fin1a2s  10336  ioounsn  13405  snunioo  13406  snunico  13407  snunioc  13408  leexp1ad  14111  exple1  14112  leexp2rd  14190  facubnd  14235  permnn  14261  sqgcd  16501  expgcd  16502  cncongr2  16607  prmdvdsbc  16665  hashgcdlem  16727  ramlb  16959  0ram  16960  ram0  16962  ramz2  16964  ramz  16965  ramcl  16969  lsmub1x  19587  lsmub2x  19588  lsmsubm  19594  pgpfac1lem2  20018  mptscmfsupp0  20890  2idlcpblrng  21238  xrsdsreclblem  21379  pzriprnglem12  21459  uvcff  21758  uvcresum  21760  frlmup1  21765  psrass1lem  21900  psrlidm  21929  psrridm  21930  psrcom  21935  mvrcl  21959  mplsubrglem  21971  mplcoe5  22007  mplbas2  22009  psrbagev1  22044  evlslem3  22047  evlslem6  22048  psropprmul  22190  evls1fpws  22325  smadiadetg  22629  cayhamlem4  22844  lecldbas  23175  pnfnei  23176  mnfnei  23177  clsconn  23386  txcls  23560  ufldom  23918  hauspwpwf1  23943  flfcnp  23960  flfcnp2  23963  cnpfcfi  23996  tsmsmhm  24102  met2ndci  24478  nghmco  24694  nghmplusg  24696  icopnfcld  24723  iocmnfcld  24724  tgioo  24752  reconnlem1  24783  metdseq0  24811  ovolunnul  25469  volinun  25515  volfiniun  25516  volsup  25525  icombl  25533  ioombl  25534  ovolioo  25537  ioorcl2  25541  volivth  25576  ismbf3d  25623  dvferm2lem  25958  lhop  25989  tayl0  26337  pserulm  26399  cxpcn3  26726  ssscongptld  26800  heron  26816  mpodvdsmulf1o  27172  dvdsmulf1o  27174  logexprlim  27204  perfectlem2  27209  lgssq  27316  lgssq2  27317  gausslemma2dlem7  27352  lgsquad2lem1  27363  lgsquad2lem2  27364  2sqblem  27410  addsq2nreurex  27423  ostth2lem2  27613  ostth3  27617  bdayfinbndlem1  28475  ubthlem2  30958  nmopleid  32226  elsuppfnd  32771  fsuppcurry1  32813  fsuppcurry2  32814  znumd  32903  zdend  32904  numdenneg  32905  mgcf1olem1  33093  mgcf1olem2  33094  gsummptres2  33146  archirngz  33282  archiabllem1a  33284  elrgspnlem2  33336  elrgspnlem3  33337  q1pdir  33695  q1pvsca  33696  ply1degltdimlem  33799  fedgmullem1  33806  fedgmullem2  33807  evls1fldgencl  33847  cos9thpiminplylem1  33959  cos9thpiminplylem2  33960  submatminr1  33987  locfinreflem  34017  sxbrsigalem2  34463  elmrsubrn  35733  ismblfin  37901  itg2gt0cn  37915  cntotbnd  38036  ismtyhmeolem  38044  heibor1lem  38049  heiborlem6  38056  rrnequiv  38075  1cvrat  39841  ps-2b  39847  2at0mat0  39890  ps-2c  39893  llncvrlpln2  39922  2llnmeqat  39936  4atlem10  39971  4atlem11a  39972  4atlem12a  39975  2lplnja  39984  dalemcea  40025  dalem2  40026  dalem21  40059  dalem54  40091  2lnat  40149  cdlemb  40159  elpaddat  40169  paddasslem7  40191  paddasslem9  40193  paddasslem10  40194  paddasslem15  40199  poml6N  40320  osumcllem6N  40326  osumcllem7N  40327  pexmidlem4N  40338  pl42lem4N  40347  lhplt  40365  lhpjat1  40385  cdlemc5  40560  cdlemeg46fgN  40899  cdlemg12g  41014  tendoco2  41133  tendococl  41137  tendodi1  41149  tendoicl  41161  cdlemi2  41184  tendospdi1  41385  dihord11c  41589  dihmeetlem6  41674  dihjatc1  41676  dihmeetlem10N  41681  fltnltalem  43009  jm2.20nn  43343  kercvrlsm  43429  omord2lim  43646  frege96d  44094  frege98d  44098  ntrclsk3  44415  snunioo1  45861  limcleqr  45991  dvdivbd  46270  volioc  46319  iblspltprt  46320  volico  46330  stoweidlem1  46348  stoweidlem24  46371  etransclem23  46604  submodlt  47699  iccpartipre  47770  2pwp1prm  47938  perfectALTVlem2  48071  lincresunit2  48827  expnegico01  48867  itscnhlinecirc02plem3  49133