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  9289  coftr  10187  fin1a2s  10328  ioounsn  13397  snunioo  13398  snunico  13399  snunioc  13400  leexp1ad  14103  exple1  14104  leexp2rd  14182  facubnd  14227  permnn  14253  sqgcd  16493  expgcd  16494  cncongr2  16599  prmdvdsbc  16657  hashgcdlem  16719  ramlb  16951  0ram  16952  ram0  16954  ramz2  16956  ramz  16957  ramcl  16961  lsmub1x  19579  lsmub2x  19580  lsmsubm  19586  pgpfac1lem2  20010  mptscmfsupp0  20882  2idlcpblrng  21230  xrsdsreclblem  21371  pzriprnglem12  21451  uvcff  21750  uvcresum  21752  frlmup1  21757  psrass1lem  21892  psrlidm  21921  psrridm  21922  psrcom  21927  mvrcl  21951  mplsubrglem  21963  mplcoe5  21999  mplbas2  22001  psrbagev1  22036  evlslem3  22039  evlslem6  22040  psropprmul  22182  evls1fpws  22317  smadiadetg  22621  cayhamlem4  22836  lecldbas  23167  pnfnei  23168  mnfnei  23169  clsconn  23378  txcls  23552  ufldom  23910  hauspwpwf1  23935  flfcnp  23952  flfcnp2  23955  cnpfcfi  23988  tsmsmhm  24094  met2ndci  24470  nghmco  24686  nghmplusg  24688  icopnfcld  24715  iocmnfcld  24716  tgioo  24744  reconnlem1  24775  metdseq0  24803  ovolunnul  25461  volinun  25507  volfiniun  25508  volsup  25517  icombl  25525  ioombl  25526  ovolioo  25529  ioorcl2  25533  volivth  25568  ismbf3d  25615  dvferm2lem  25950  lhop  25981  tayl0  26329  pserulm  26391  cxpcn3  26718  ssscongptld  26792  heron  26808  mpodvdsmulf1o  27164  dvdsmulf1o  27166  logexprlim  27196  perfectlem2  27201  lgssq  27308  lgssq2  27309  gausslemma2dlem7  27344  lgsquad2lem1  27355  lgsquad2lem2  27356  2sqblem  27402  addsq2nreurex  27415  ostth2lem2  27605  ostth3  27609  bdayfinbndlem1  28446  ubthlem2  30929  nmopleid  32197  elsuppfnd  32742  fsuppcurry1  32784  fsuppcurry2  32785  znumd  32874  zdend  32875  numdenneg  32876  mgcf1olem1  33064  mgcf1olem2  33065  gsummptres2  33117  archirngz  33252  archiabllem1a  33254  elrgspnlem2  33306  elrgspnlem3  33307  q1pdir  33665  q1pvsca  33666  ply1degltdimlem  33760  fedgmullem1  33767  fedgmullem2  33768  evls1fldgencl  33808  cos9thpiminplylem1  33920  cos9thpiminplylem2  33921  submatminr1  33948  locfinreflem  33978  sxbrsigalem2  34424  elmrsubrn  35695  ismblfin  37833  itg2gt0cn  37847  cntotbnd  37968  ismtyhmeolem  37976  heibor1lem  37981  heiborlem6  37988  rrnequiv  38007  1cvrat  39773  ps-2b  39779  2at0mat0  39822  ps-2c  39825  llncvrlpln2  39854  2llnmeqat  39868  4atlem10  39903  4atlem11a  39904  4atlem12a  39907  2lplnja  39916  dalemcea  39957  dalem2  39958  dalem21  39991  dalem54  40023  2lnat  40081  cdlemb  40091  elpaddat  40101  paddasslem7  40123  paddasslem9  40125  paddasslem10  40126  paddasslem15  40131  poml6N  40252  osumcllem6N  40258  osumcllem7N  40259  pexmidlem4N  40270  pl42lem4N  40279  lhplt  40297  lhpjat1  40317  cdlemc5  40492  cdlemeg46fgN  40831  cdlemg12g  40946  tendoco2  41065  tendococl  41069  tendodi1  41081  tendoicl  41093  cdlemi2  41116  tendospdi1  41317  dihord11c  41521  dihmeetlem6  41606  dihjatc1  41608  dihmeetlem10N  41613  fltnltalem  42941  jm2.20nn  43275  kercvrlsm  43361  omord2lim  43578  frege96d  44026  frege98d  44030  ntrclsk3  44347  snunioo1  45794  limcleqr  45924  dvdivbd  46203  volioc  46252  iblspltprt  46253  volico  46263  stoweidlem1  46281  stoweidlem24  46304  etransclem23  46537  submodlt  47632  iccpartipre  47703  2pwp1prm  47871  perfectALTVlem2  48004  lincresunit2  48760  expnegico01  48800  itscnhlinecirc02plem3  49066