Theorem syl32anc 1378

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 1373	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  9451  coftr  10342  fin1a2s  10483  ioounsn  13537  snunioo  13538  snunico  13539  snunioc  13540  exple1  14226  leexp2rd  14304  facubnd  14349  permnn  14375  sqgcd  16609  expgcd  16610  cncongr2  16715  prmdvdsbc  16773  hashgcdlem  16835  ramlb  17066  0ram  17067  ram0  17069  ramz2  17071  ramz  17072  ramcl  17076  lsmub1x  19688  lsmub2x  19689  lsmsubm  19695  pgpfac1lem2  20119  mptscmfsupp0  20947  2idlcpblrng  21304  xrsdsreclblem  21453  pzriprnglem12  21526  uvcff  21834  uvcresum  21836  frlmup1  21841  psrass1lem  21975  psrlidm  22005  psrridm  22006  psrcom  22011  mvrcl  22035  mplsubrglem  22047  mplcoe5  22081  mplbas2  22083  psrbagev1  22124  evlslem3  22127  evlslem6  22128  psropprmul  22260  evls1fpws  22394  smadiadetg  22700  cayhamlem4  22915  lecldbas  23248  pnfnei  23249  mnfnei  23250  clsconn  23459  txcls  23633  ufldom  23991  hauspwpwf1  24016  flfcnp  24033  flfcnp2  24036  cnpfcfi  24069  tsmsmhm  24175  met2ndci  24556  nghmco  24780  nghmplusg  24782  icopnfcld  24809  iocmnfcld  24810  tgioo  24837  reconnlem1  24867  metdseq0  24895  ovolunnul  25554  volinun  25600  volfiniun  25601  volsup  25610  icombl  25618  ioombl  25619  ovolioo  25622  ioorcl2  25626  volivth  25661  ismbf3d  25708  dvferm2lem  26044  lhop  26075  tayl0  26421  pserulm  26483  cxpcn3  26809  ssscongptld  26883  heron  26899  mpodvdsmulf1o  27255  dvdsmulf1o  27257  logexprlim  27287  perfectlem2  27292  lgssq  27399  lgssq2  27400  gausslemma2dlem7  27435  lgsquad2lem1  27446  lgsquad2lem2  27447  2sqblem  27493  addsq2nreurex  27506  ostth2lem2  27696  ostth3  27700  ubthlem2  30903  nmopleid  32171  fsuppcurry1  32739  fsuppcurry2  32740  znumd  32816  zdend  32817  numdenneg  32818  mgcf1olem1  32974  mgcf1olem2  32975  gsummptres2  33036  archirngz  33169  archiabllem1a  33171  q1pdir  33588  q1pvsca  33589  ply1degltdimlem  33635  fedgmullem1  33642  fedgmullem2  33643  evls1fldgencl  33680  submatminr1  33756  locfinreflem  33786  sxbrsigalem2  34251  elmrsubrn  35488  ismblfin  37621  itg2gt0cn  37635  cntotbnd  37756  ismtyhmeolem  37764  heibor1lem  37769  heiborlem6  37776  rrnequiv  37795  1cvrat  39433  ps-2b  39439  2at0mat0  39482  ps-2c  39485  llncvrlpln2  39514  2llnmeqat  39528  4atlem10  39563  4atlem11a  39564  4atlem12a  39567  2lplnja  39576  dalemcea  39617  dalem2  39618  dalem21  39651  dalem54  39683  2lnat  39741  cdlemb  39751  elpaddat  39761  paddasslem7  39783  paddasslem9  39785  paddasslem10  39786  paddasslem15  39791  poml6N  39912  osumcllem6N  39918  osumcllem7N  39919  pexmidlem4N  39930  pl42lem4N  39939  lhplt  39957  lhpjat1  39977  cdlemc5  40152  cdlemeg46fgN  40491  cdlemg12g  40606  tendoco2  40725  tendococl  40729  tendodi1  40741  tendoicl  40753  cdlemi2  40776  tendospdi1  40977  dihord11c  41181  dihmeetlem6  41266  dihjatc1  41268  dihmeetlem10N  41273  fltnltalem  42617  jm2.20nn  42954  kercvrlsm  43040  omord2lim  43262  frege96d  43711  frege98d  43715  ntrclsk3  44032  snunioo1  45430  limcleqr  45565  dvdivbd  45844  volioc  45893  iblspltprt  45894  volico  45904  stoweidlem1  45922  stoweidlem24  45945  etransclem23  46178  iccpartipre  47295  2pwp1prm  47463  perfectALTVlem2  47596  lincresunit2  48207  expnegico01  48247  itscnhlinecirc02plem3  48518