Theorem syl32anc 1401

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  fsuppsssuppgd  9330  coftr  10245  fin1a2s  10386  ioounsn  13495  snunioo  13496  snunico  13497  snunioc  13498  leexp1ad  14203  exple1  14204  leexp2rd  14282  facubnd  14327  permnn  14353  sqgcd  16610  expgcd  16611  cncongr2  16716  prmdvdsbc  16775  hashgcdlem  16837  ramlb  17069  0ram  17070  ram0  17072  ramz2  17074  ramz  17075  ramcl  17079  lsmub1x  19707  lsmub2x  19708  lsmsubm  19714  pgpfac1lem2  20138  mptscmfsupp0  21017  2idlcpblrng  21372  xrsdsreclblem  21523  pzriprnglem12  21602  uvcff  21901  uvcresum  21903  frlmup1  21908  psrass1lem  22043  psrlidm  22071  psrridm  22072  psrcom  22077  mvrcl  22101  mplsubrglem  22113  mplcoe5  22151  mplbas2  22153  psrbagev1  22188  evlslem3  22191  evlslem6  22192  psropprmul  22357  evls1fpws  22490  smadiadetg  22791  cayhamlem4  23006  lecldbas  23337  pnfnei  23338  mnfnei  23339  clsconn  23548  txcls  23722  ufldom  24080  hauspwpwf1  24105  flfcnp  24122  flfcnp2  24125  cnpfcfi  24158  tsmsmhm  24264  met2ndci  24640  nghmco  24856  nghmplusg  24858  icopnfcld  24885  iocmnfcld  24886  tgioo  24914  reconnlem1  24945  metdseq0  24973  ovolunnul  25620  volinun  25666  volfiniun  25667  volsup  25676  icombl  25684  ioombl  25685  ovolioo  25688  ioorcl2  25692  volivth  25727  ismbf3d  25774  dvferm2lem  26106  lhop  26136  tayl0  26483  pserulm  26543  cxpcn3  26871  ssscongptld  26945  heron  26961  mpodvdsmulf1o  27316  dvdsmulf1o  27318  logexprlim  27347  perfectlem2  27352  lgssq  27459  lgssq2  27460  gausslemma2dlem7  27495  lgsquad2lem1  27506  lgsquad2lem2  27507  2sqblem  27553  addsq2nreurex  27566  ostth2lem2  27756  ostth3  27760  bdayfinbndlem1  28618  ubthlem2  31132  nmopleid  32400  elsuppfnd  32939  fsuppcurry1  32981  fsuppcurry2  32982  znumd  33070  zdend  33071  numdenneg  33072  mgcf1olem1  33234  mgcf1olem2  33235  gsummptres2  33286  archirngz  33422  archiabllem1a  33424  elrgspnlem2  33476  elrgspnlem3  33477  q1pdir  33810  q1pvsca  33811  ply1degltdimlem  33929  fedgmullem1  33936  fedgmullem2  33937  evls1fldgencl  33977  cos9thpiminplylem1  34089  cos9thpiminplylem2  34090  submatminr1  34117  locfinreflem  34147  sxbrsigalem2  34593  elmrsubrn  35883  ismblfin  38172  itg2gt0cn  38186  cntotbnd  38307  ismtyhmeolem  38315  heibor1lem  38320  heiborlem6  38327  rrnequiv  38346  1cvrat  40112  ps-2b  40118  2at0mat0  40161  ps-2c  40164  llncvrlpln2  40193  2llnmeqat  40207  4atlem10  40242  4atlem11a  40243  4atlem12a  40246  2lplnja  40255  dalemcea  40296  dalem2  40297  dalem21  40330  dalem54  40362  2lnat  40420  cdlemb  40430  elpaddat  40440  paddasslem7  40462  paddasslem9  40464  paddasslem10  40465  paddasslem15  40470  poml6N  40591  osumcllem6N  40597  osumcllem7N  40598  pexmidlem4N  40609  pl42lem4N  40618  lhplt  40636  lhpjat1  40656  cdlemc5  40831  cdlemeg46fgN  41170  cdlemg12g  41285  tendoco2  41404  tendococl  41408  tendodi1  41420  tendoicl  41432  cdlemi2  41455  tendospdi1  41656  dihord11c  41860  dihmeetlem6  41945  dihjatc1  41947  dihmeetlem10N  41952  fltnltalem  43256  jm2.20nn  43586  kercvrlsm  43672  omord2lim  43889  frege96d  44337  frege98d  44341  ntrclsk3  44658  snunioo1  46086  limcleqr  46216  dvdivbd  46495  volioc  46544  iblspltprt  46545  volico  46555  stoweidlem1  46573  stoweidlem24  46596  etransclem23  46829  submodlt  47948  iccpartipre  48025  2pwp1prm  48196  perfectALTVlem2  48342  lincresunit2  49109  expnegico01  49149  itscnhlinecirc02plem3  49415