Theorem syl32anc 1377

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 1372	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  fsuppsssuppgd  9419  coftr  10310  fin1a2s  10451  ioounsn  13513  snunioo  13514  snunico  13515  snunioc  13516  exple1  14212  leexp2rd  14290  facubnd  14335  permnn  14361  sqgcd  16595  expgcd  16596  cncongr2  16701  prmdvdsbc  16759  hashgcdlem  16821  ramlb  17052  0ram  17053  ram0  17055  ramz2  17057  ramz  17058  ramcl  17062  lsmub1x  19678  lsmub2x  19679  lsmsubm  19685  pgpfac1lem2  20109  mptscmfsupp0  20941  2idlcpblrng  21298  xrsdsreclblem  21447  pzriprnglem12  21520  uvcff  21828  uvcresum  21830  frlmup1  21835  psrass1lem  21969  psrlidm  21999  psrridm  22000  psrcom  22005  mvrcl  22029  mplsubrglem  22041  mplcoe5  22075  mplbas2  22077  psrbagev1  22118  evlslem3  22121  evlslem6  22122  psropprmul  22254  evls1fpws  22388  smadiadetg  22694  cayhamlem4  22909  lecldbas  23242  pnfnei  23243  mnfnei  23244  clsconn  23453  txcls  23627  ufldom  23985  hauspwpwf1  24010  flfcnp  24027  flfcnp2  24030  cnpfcfi  24063  tsmsmhm  24169  met2ndci  24550  nghmco  24774  nghmplusg  24776  icopnfcld  24803  iocmnfcld  24804  tgioo  24831  reconnlem1  24861  metdseq0  24889  ovolunnul  25548  volinun  25594  volfiniun  25595  volsup  25604  icombl  25612  ioombl  25613  ovolioo  25616  ioorcl2  25620  volivth  25655  ismbf3d  25702  dvferm2lem  26038  lhop  26069  tayl0  26417  pserulm  26479  cxpcn3  26805  ssscongptld  26879  heron  26895  mpodvdsmulf1o  27251  dvdsmulf1o  27253  logexprlim  27283  perfectlem2  27288  lgssq  27395  lgssq2  27396  gausslemma2dlem7  27431  lgsquad2lem1  27442  lgsquad2lem2  27443  2sqblem  27489  addsq2nreurex  27502  ostth2lem2  27692  ostth3  27696  ubthlem2  30899  nmopleid  32167  elsuppfnd  32696  fsuppcurry1  32742  fsuppcurry2  32743  znumd  32818  zdend  32819  numdenneg  32820  mgcf1olem1  32975  mgcf1olem2  32976  gsummptres2  33038  archirngz  33178  archiabllem1a  33180  elrgspnlem2  33232  elrgspnlem3  33233  q1pdir  33602  q1pvsca  33603  ply1degltdimlem  33649  fedgmullem1  33656  fedgmullem2  33657  evls1fldgencl  33694  submatminr1  33770  locfinreflem  33800  sxbrsigalem2  34267  elmrsubrn  35504  ismblfin  37647  itg2gt0cn  37661  cntotbnd  37782  ismtyhmeolem  37790  heibor1lem  37795  heiborlem6  37802  rrnequiv  37821  1cvrat  39458  ps-2b  39464  2at0mat0  39507  ps-2c  39510  llncvrlpln2  39539  2llnmeqat  39553  4atlem10  39588  4atlem11a  39589  4atlem12a  39592  2lplnja  39601  dalemcea  39642  dalem2  39643  dalem21  39676  dalem54  39708  2lnat  39766  cdlemb  39776  elpaddat  39786  paddasslem7  39808  paddasslem9  39810  paddasslem10  39811  paddasslem15  39816  poml6N  39937  osumcllem6N  39943  osumcllem7N  39944  pexmidlem4N  39955  pl42lem4N  39964  lhplt  39982  lhpjat1  40002  cdlemc5  40177  cdlemeg46fgN  40516  cdlemg12g  40631  tendoco2  40750  tendococl  40754  tendodi1  40766  tendoicl  40778  cdlemi2  40801  tendospdi1  41002  dihord11c  41206  dihmeetlem6  41291  dihjatc1  41293  dihmeetlem10N  41298  fltnltalem  42648  jm2.20nn  42985  kercvrlsm  43071  omord2lim  43289  frege96d  43738  frege98d  43742  ntrclsk3  44059  snunioo1  45464  limcleqr  45599  dvdivbd  45878  volioc  45927  iblspltprt  45928  volico  45938  stoweidlem1  45956  stoweidlem24  45979  etransclem23  46212  submodlt  47289  iccpartipre  47345  2pwp1prm  47513  perfectALTVlem2  47646  lincresunit2  48323  expnegico01  48363  itscnhlinecirc02plem3  48633