Theorem syl32anc 1386

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  fsuppsssuppgd  9292  coftr  10193  fin1a2s  10334  ioounsn  13428  snunioo  13429  snunico  13430  snunioc  13431  leexp1ad  14136  exple1  14137  leexp2rd  14215  facubnd  14260  permnn  14286  sqgcd  16529  expgcd  16530  cncongr2  16635  prmdvdsbc  16694  hashgcdlem  16756  ramlb  16988  0ram  16989  ram0  16991  ramz2  16993  ramz  16994  ramcl  16998  lsmub1x  19619  lsmub2x  19620  lsmsubm  19626  pgpfac1lem2  20050  mptscmfsupp0  20924  2idlcpblrng  21271  xrsdsreclblem  21395  pzriprnglem12  21474  uvcff  21773  uvcresum  21775  frlmup1  21780  psrass1lem  21915  psrlidm  21943  psrridm  21944  psrcom  21949  mvrcl  21973  mplsubrglem  21985  mplcoe5  22023  mplbas2  22025  psrbagev1  22060  evlslem3  22063  evlslem6  22064  psropprmul  22229  evls1fpws  22362  smadiadetg  22663  cayhamlem4  22878  lecldbas  23209  pnfnei  23210  mnfnei  23211  clsconn  23420  txcls  23594  ufldom  23952  hauspwpwf1  23977  flfcnp  23994  flfcnp2  23997  cnpfcfi  24030  tsmsmhm  24136  met2ndci  24512  nghmco  24728  nghmplusg  24730  icopnfcld  24757  iocmnfcld  24758  tgioo  24786  reconnlem1  24817  metdseq0  24845  ovolunnul  25492  volinun  25538  volfiniun  25539  volsup  25548  icombl  25556  ioombl  25557  ovolioo  25560  ioorcl2  25564  volivth  25599  ismbf3d  25646  dvferm2lem  25978  lhop  26008  tayl0  26352  pserulm  26412  cxpcn3  26737  ssscongptld  26811  heron  26827  mpodvdsmulf1o  27182  dvdsmulf1o  27184  logexprlim  27213  perfectlem2  27218  lgssq  27325  lgssq2  27326  gausslemma2dlem7  27361  lgsquad2lem1  27372  lgsquad2lem2  27373  2sqblem  27419  addsq2nreurex  27432  ostth2lem2  27622  ostth3  27626  bdayfinbndlem1  28484  ubthlem2  30967  nmopleid  32235  elsuppfnd  32781  fsuppcurry1  32823  fsuppcurry2  32824  znumd  32912  zdend  32913  numdenneg  32914  mgcf1olem1  33087  mgcf1olem2  33088  gsummptres2  33141  archirngz  33277  archiabllem1a  33279  elrgspnlem2  33331  elrgspnlem3  33332  q1pdir  33693  q1pvsca  33694  ply1degltdimlem  33813  fedgmullem1  33820  fedgmullem2  33821  evls1fldgencl  33861  cos9thpiminplylem1  33973  cos9thpiminplylem2  33974  submatminr1  34001  locfinreflem  34031  sxbrsigalem2  34477  elmrsubrn  35749  ismblfin  38029  itg2gt0cn  38043  cntotbnd  38164  ismtyhmeolem  38172  heibor1lem  38177  heiborlem6  38184  rrnequiv  38203  1cvrat  39969  ps-2b  39975  2at0mat0  40018  ps-2c  40021  llncvrlpln2  40050  2llnmeqat  40064  4atlem10  40099  4atlem11a  40100  4atlem12a  40103  2lplnja  40112  dalemcea  40153  dalem2  40154  dalem21  40187  dalem54  40219  2lnat  40277  cdlemb  40287  elpaddat  40297  paddasslem7  40319  paddasslem9  40321  paddasslem10  40322  paddasslem15  40327  poml6N  40448  osumcllem6N  40454  osumcllem7N  40455  pexmidlem4N  40466  pl42lem4N  40475  lhplt  40493  lhpjat1  40513  cdlemc5  40688  cdlemeg46fgN  41027  cdlemg12g  41142  tendoco2  41261  tendococl  41265  tendodi1  41277  tendoicl  41289  cdlemi2  41312  tendospdi1  41513  dihord11c  41717  dihmeetlem6  41802  dihjatc1  41804  dihmeetlem10N  41809  fltnltalem  43113  jm2.20nn  43443  kercvrlsm  43529  omord2lim  43746  frege96d  44194  frege98d  44198  ntrclsk3  44515  snunioo1  45958  limcleqr  46088  dvdivbd  46367  volioc  46416  iblspltprt  46417  volico  46427  stoweidlem1  46445  stoweidlem24  46468  etransclem23  46701  submodlt  47820  iccpartipre  47897  2pwp1prm  48068  perfectALTVlem2  48214  lincresunit2  48970  expnegico01  49010  itscnhlinecirc02plem3  49276