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  9295  coftr  10195  fin1a2s  10336  ioounsn  13430  snunioo  13431  snunico  13432  snunioc  13433  leexp1ad  14138  exple1  14139  leexp2rd  14217  facubnd  14262  permnn  14288  sqgcd  16531  expgcd  16532  cncongr2  16637  prmdvdsbc  16696  hashgcdlem  16758  ramlb  16990  0ram  16991  ram0  16993  ramz2  16995  ramz  16996  ramcl  17000  lsmub1x  19621  lsmub2x  19622  lsmsubm  19628  pgpfac1lem2  20052  mptscmfsupp0  20922  2idlcpblrng  21269  xrsdsreclblem  21393  pzriprnglem12  21472  uvcff  21771  uvcresum  21773  frlmup1  21778  psrass1lem  21912  psrlidm  21940  psrridm  21941  psrcom  21946  mvrcl  21970  mplsubrglem  21982  mplcoe5  22018  mplbas2  22020  psrbagev1  22055  evlslem3  22058  evlslem6  22059  psropprmul  22201  evls1fpws  22334  smadiadetg  22638  cayhamlem4  22853  lecldbas  23184  pnfnei  23185  mnfnei  23186  clsconn  23395  txcls  23569  ufldom  23927  hauspwpwf1  23952  flfcnp  23969  flfcnp2  23972  cnpfcfi  24005  tsmsmhm  24111  met2ndci  24487  nghmco  24703  nghmplusg  24705  icopnfcld  24732  iocmnfcld  24733  tgioo  24761  reconnlem1  24792  metdseq0  24820  ovolunnul  25467  volinun  25513  volfiniun  25514  volsup  25523  icombl  25531  ioombl  25532  ovolioo  25535  ioorcl2  25539  volivth  25574  ismbf3d  25621  dvferm2lem  25953  lhop  25983  tayl0  26327  pserulm  26387  cxpcn3  26712  ssscongptld  26786  heron  26802  mpodvdsmulf1o  27157  dvdsmulf1o  27159  logexprlim  27188  perfectlem2  27193  lgssq  27300  lgssq2  27301  gausslemma2dlem7  27336  lgsquad2lem1  27347  lgsquad2lem2  27348  2sqblem  27394  addsq2nreurex  27407  ostth2lem2  27597  ostth3  27601  bdayfinbndlem1  28459  ubthlem2  30942  nmopleid  32210  elsuppfnd  32755  fsuppcurry1  32797  fsuppcurry2  32798  znumd  32886  zdend  32887  numdenneg  32888  mgcf1olem1  33061  mgcf1olem2  33062  gsummptres2  33114  archirngz  33250  archiabllem1a  33252  elrgspnlem2  33304  elrgspnlem3  33305  q1pdir  33663  q1pvsca  33664  ply1degltdimlem  33766  fedgmullem1  33773  fedgmullem2  33774  evls1fldgencl  33814  cos9thpiminplylem1  33926  cos9thpiminplylem2  33927  submatminr1  33954  locfinreflem  33984  sxbrsigalem2  34430  elmrsubrn  35702  ismblfin  37982  itg2gt0cn  37996  cntotbnd  38117  ismtyhmeolem  38125  heibor1lem  38130  heiborlem6  38137  rrnequiv  38156  1cvrat  39922  ps-2b  39928  2at0mat0  39971  ps-2c  39974  llncvrlpln2  40003  2llnmeqat  40017  4atlem10  40052  4atlem11a  40053  4atlem12a  40056  2lplnja  40065  dalemcea  40106  dalem2  40107  dalem21  40140  dalem54  40172  2lnat  40230  cdlemb  40240  elpaddat  40250  paddasslem7  40272  paddasslem9  40274  paddasslem10  40275  paddasslem15  40280  poml6N  40401  osumcllem6N  40407  osumcllem7N  40408  pexmidlem4N  40419  pl42lem4N  40428  lhplt  40446  lhpjat1  40466  cdlemc5  40641  cdlemeg46fgN  40980  cdlemg12g  41095  tendoco2  41214  tendococl  41218  tendodi1  41230  tendoicl  41242  cdlemi2  41265  tendospdi1  41466  dihord11c  41670  dihmeetlem6  41755  dihjatc1  41757  dihmeetlem10N  41762  fltnltalem  43095  jm2.20nn  43425  kercvrlsm  43511  omord2lim  43728  frege96d  44176  frege98d  44180  ntrclsk3  44497  snunioo1  45942  limcleqr  46072  dvdivbd  46351  volioc  46400  iblspltprt  46401  volico  46411  stoweidlem1  46429  stoweidlem24  46452  etransclem23  46685  submodlt  47798  iccpartipre  47875  2pwp1prm  48046  perfectALTVlem2  48192  lincresunit2  48948  expnegico01  48988  itscnhlinecirc02plem3  49254