Theorem syl32anc 1380

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 1375	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  9422  coftr  10313  fin1a2s  10454  ioounsn  13517  snunioo  13518  snunico  13519  snunioc  13520  exple1  14216  leexp2rd  14294  facubnd  14339  permnn  14365  sqgcd  16599  expgcd  16600  cncongr2  16705  prmdvdsbc  16763  hashgcdlem  16825  ramlb  17057  0ram  17058  ram0  17060  ramz2  17062  ramz  17063  ramcl  17067  lsmub1x  19664  lsmub2x  19665  lsmsubm  19671  pgpfac1lem2  20095  mptscmfsupp0  20925  2idlcpblrng  21281  xrsdsreclblem  21430  pzriprnglem12  21503  uvcff  21811  uvcresum  21813  frlmup1  21818  psrass1lem  21952  psrlidm  21982  psrridm  21983  psrcom  21988  mvrcl  22012  mplsubrglem  22024  mplcoe5  22058  mplbas2  22060  psrbagev1  22101  evlslem3  22104  evlslem6  22105  psropprmul  22239  evls1fpws  22373  smadiadetg  22679  cayhamlem4  22894  lecldbas  23227  pnfnei  23228  mnfnei  23229  clsconn  23438  txcls  23612  ufldom  23970  hauspwpwf1  23995  flfcnp  24012  flfcnp2  24015  cnpfcfi  24048  tsmsmhm  24154  met2ndci  24535  nghmco  24759  nghmplusg  24761  icopnfcld  24788  iocmnfcld  24789  tgioo  24817  reconnlem1  24848  metdseq0  24876  ovolunnul  25535  volinun  25581  volfiniun  25582  volsup  25591  icombl  25599  ioombl  25600  ovolioo  25603  ioorcl2  25607  volivth  25642  ismbf3d  25689  dvferm2lem  26024  lhop  26055  tayl0  26403  pserulm  26465  cxpcn3  26791  ssscongptld  26865  heron  26881  mpodvdsmulf1o  27237  dvdsmulf1o  27239  logexprlim  27269  perfectlem2  27274  lgssq  27381  lgssq2  27382  gausslemma2dlem7  27417  lgsquad2lem1  27428  lgsquad2lem2  27429  2sqblem  27475  addsq2nreurex  27488  ostth2lem2  27678  ostth3  27682  ubthlem2  30890  nmopleid  32158  elsuppfnd  32691  fsuppcurry1  32736  fsuppcurry2  32737  znumd  32814  zdend  32815  numdenneg  32816  mgcf1olem1  32991  mgcf1olem2  32992  gsummptres2  33056  archirngz  33196  archiabllem1a  33198  elrgspnlem2  33247  elrgspnlem3  33248  q1pdir  33623  q1pvsca  33624  ply1degltdimlem  33673  fedgmullem1  33680  fedgmullem2  33681  evls1fldgencl  33720  submatminr1  33809  locfinreflem  33839  sxbrsigalem2  34288  elmrsubrn  35525  ismblfin  37668  itg2gt0cn  37682  cntotbnd  37803  ismtyhmeolem  37811  heibor1lem  37816  heiborlem6  37823  rrnequiv  37842  1cvrat  39478  ps-2b  39484  2at0mat0  39527  ps-2c  39530  llncvrlpln2  39559  2llnmeqat  39573  4atlem10  39608  4atlem11a  39609  4atlem12a  39612  2lplnja  39621  dalemcea  39662  dalem2  39663  dalem21  39696  dalem54  39728  2lnat  39786  cdlemb  39796  elpaddat  39806  paddasslem7  39828  paddasslem9  39830  paddasslem10  39831  paddasslem15  39836  poml6N  39957  osumcllem6N  39963  osumcllem7N  39964  pexmidlem4N  39975  pl42lem4N  39984  lhplt  40002  lhpjat1  40022  cdlemc5  40197  cdlemeg46fgN  40536  cdlemg12g  40651  tendoco2  40770  tendococl  40774  tendodi1  40786  tendoicl  40798  cdlemi2  40821  tendospdi1  41022  dihord11c  41226  dihmeetlem6  41311  dihjatc1  41313  dihmeetlem10N  41318  fltnltalem  42672  jm2.20nn  43009  kercvrlsm  43095  omord2lim  43313  frege96d  43762  frege98d  43766  ntrclsk3  44083  snunioo1  45525  limcleqr  45659  dvdivbd  45938  volioc  45987  iblspltprt  45988  volico  45998  stoweidlem1  46016  stoweidlem24  46039  etransclem23  46272  submodlt  47352  iccpartipre  47408  2pwp1prm  47576  perfectALTVlem2  47709  lincresunit2  48395  expnegico01  48435  itscnhlinecirc02plem3  48705