Theorem syl32anc 1379

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 513	. 2 ⊢ (𝜑 → (𝜏 ∧ 𝜂))
7		syl32anc.6	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁)
8	1, 2, 3, 6, 7	syl31anc 1374	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  coftr  10268  fin1a2s  10409  ioounsn  13454  snunioo  13455  snunico  13456  snunioc  13457  exple1  14141  leexp2rd  14218  facubnd  14260  permnn  14286  sqgcd  16502  cncongr2  16605  hashgcdlem  16721  ramlb  16952  0ram  16953  ram0  16955  ramz2  16957  ramz  16958  ramcl  16962  lsmub1x  19514  lsmub2x  19515  lsmsubm  19521  pgpfac1lem2  19945  mptscmfsupp0  20537  xrsdsreclblem  20991  uvcff  21346  uvcresum  21348  frlmup1  21353  psrass1lemOLD  21493  psrass1lem  21496  psrlidm  21523  psrridm  21524  psrcom  21529  mvrcl  21551  mplsubrglem  21563  mplcoe5  21595  mplbas2  21597  psrbagev1  21638  psrbagev1OLD  21639  evlslem3  21643  evlslem6  21644  psropprmul  21760  smadiadetg  22175  cayhamlem4  22390  lecldbas  22723  pnfnei  22724  mnfnei  22725  clsconn  22934  txcls  23108  ufldom  23466  hauspwpwf1  23491  flfcnp  23508  flfcnp2  23511  cnpfcfi  23544  tsmsmhm  23650  met2ndci  24031  nghmco  24255  nghmplusg  24257  icopnfcld  24284  iocmnfcld  24285  tgioo  24312  reconnlem1  24342  metdseq0  24370  ovolunnul  25017  volinun  25063  volfiniun  25064  volsup  25073  icombl  25081  ioombl  25082  ovolioo  25085  ioorcl2  25089  volivth  25124  ismbf3d  25171  dvferm2lem  25503  lhop  25533  tayl0  25874  pserulm  25934  cxpcn3  26256  ssscongptld  26327  heron  26343  dvdsmulf1o  26698  logexprlim  26728  perfectlem2  26733  lgssq  26840  lgssq2  26841  gausslemma2dlem7  26876  lgsquad2lem1  26887  lgsquad2lem2  26888  2sqblem  26934  addsq2nreurex  26947  ostth2lem2  27137  ostth3  27141  ubthlem2  30124  nmopleid  31392  fsuppcurry1  31950  fsuppcurry2  31951  prmdvdsbc  32022  numdenneg  32023  mgcf1olem1  32171  mgcf1olem2  32172  gsummptres2  32205  archirngz  32335  archiabllem1a  32337  evls1fpws  32646  ply1degltdimlem  32707  fedgmullem1  32714  fedgmullem2  32715  submatminr1  32790  locfinreflem  32820  sxbrsigalem2  33285  elmrsubrn  34511  ismblfin  36529  itg2gt0cn  36543  cntotbnd  36664  ismtyhmeolem  36672  heibor1lem  36677  heiborlem6  36684  rrnequiv  36703  1cvrat  38347  ps-2b  38353  2at0mat0  38396  ps-2c  38399  llncvrlpln2  38428  2llnmeqat  38442  4atlem10  38477  4atlem11a  38478  4atlem12a  38481  2lplnja  38490  dalemcea  38531  dalem2  38532  dalem21  38565  dalem54  38597  2lnat  38655  cdlemb  38665  elpaddat  38675  paddasslem7  38697  paddasslem9  38699  paddasslem10  38700  paddasslem15  38705  poml6N  38826  osumcllem6N  38832  osumcllem7N  38833  pexmidlem4N  38844  pl42lem4N  38853  lhplt  38871  lhpjat1  38891  cdlemc5  39066  cdlemeg46fgN  39405  cdlemg12g  39520  tendoco2  39639  tendococl  39643  tendodi1  39655  tendoicl  39667  cdlemi2  39690  tendospdi1  39891  dihord11c  40095  dihmeetlem6  40180  dihjatc1  40182  dihmeetlem10N  40187  fsuppsssuppgd  41064  expgcd  41225  fltnltalem  41404  jm2.20nn  41736  kercvrlsm  41825  omord2lim  42050  frege96d  42500  frege98d  42504  ntrclsk3  42821  snunioo1  44225  limcleqr  44360  dvdivbd  44639  volioc  44688  iblspltprt  44689  volico  44699  stoweidlem1  44717  stoweidlem24  44740  etransclem23  44973  iccpartipre  46089  2pwp1prm  46257  perfectALTVlem2  46390  2idlcpblrng  46766  pzriprnglem12  46816  lincresunit2  47159  expnegico01  47199  itscnhlinecirc02plem3  47470