Theorem syl32anc 1405

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  fsuppsssuppgd  9355  coftr  10278  fin1a2s  10419  ioounsn  13532  snunioo  13533  snunico  13534  snunioc  13535  leexp1ad  14242  exple1  14243  leexp2rd  14321  facubnd  14366  permnn  14392  sqgcd  16656  expgcd  16657  cncongr2  16762  prmdvdsbc  16821  hashgcdlem  16883  ramlb  17115  0ram  17116  ram0  17118  ramz2  17120  ramz  17121  ramcl  17125  lsmub1x  19777  lsmub2x  19778  lsmsubm  19784  pgpfac1lem2  20208  mptscmfsupp0  21115  2idlcpblrng  21477  xrsdsreclblem  21630  pzriprnglem12  21709  uvcff  22008  uvcresum  22010  frlmup1  22015  psrass1lem  22152  psrlidm  22180  psrridm  22181  psrcom  22186  mvrcl  22210  mplsubrglem  22222  mplcoe5  22260  mplbas2  22262  psrbagev1  22297  evlslem3  22300  evlslem6  22301  psropprmul  22466  evls1fpws  22598  smadiadetg  22899  cayhamlem4  23117  lecldbas  23448  pnfnei  23449  mnfnei  23450  clsconn  23659  txcls  23834  ufldom  24192  hauspwpwf1  24217  flfcnp  24234  flfcnp2  24237  cnpfcfi  24270  tsmsmhm  24376  met2ndci  24752  nghmco  24968  nghmplusg  24970  icopnfcld  24997  iocmnfcld  24998  tgioo  25026  reconnlem1  25057  metdseq0  25085  ovolunnul  25732  volinun  25778  volfiniun  25779  volsup  25788  icombl  25796  ioombl  25797  ovolioo  25800  ioorcl2  25804  volivth  25839  ismbf3d  25886  dvferm2lem  26218  lhop  26248  tayl0  26598  pserulm  26658  cxpcn3  26986  ssscongptld  27060  heron  27076  mpodvdsmulf1o  27431  dvdsmulf1o  27433  logexprlim  27462  perfectlem2  27467  lgssq  27574  lgssq2  27575  gausslemma2dlem7  27610  lgsquad2lem1  27621  lgsquad2lem2  27622  2sqblem  27668  addsq2nreurex  27681  ostth2lem2  27871  ostth3  27875  bdayfinbndlem1  28733  ubthlem2  31353  nmopleid  32621  elsuppfnd  33156  fsuppcurry1  33197  fsuppcurry2  33198  znumd  33285  zdend  33286  numdenneg  33287  mgcf1olem1  33443  mgcf1olem2  33444  gsummptres2  33495  archirngz  33631  archiabllem1a  33633  elrgspnlem2  33685  elrgspnlem3  33686  q1pdir  34015  q1pvsca  34016  ply1degltdimlem  34134  fedgmullem1  34141  fedgmullem2  34142  evls1fldgencl  34182  cos9thpiminplylem1  34294  cos9thpiminplylem2  34295  submatminr1  34322  locfinreflem  34352  sxbrsigalem2  34799  elmrsubrn  36101  ismblfin  38412  itg2gt0cn  38426  cntotbnd  38548  ismtyhmeolem  38556  heibor1lem  38561  heiborlem6  38568  rrnequiv  38587  1cvrat  40351  ps-2b  40357  2at0mat0  40400  ps-2c  40403  llncvrlpln2  40432  2llnmeqat  40446  4atlem10  40481  4atlem11a  40482  4atlem12a  40485  2lplnja  40494  dalemcea  40535  dalem2  40536  dalem21  40569  dalem54  40601  2lnat  40659  cdlemb  40669  elpaddat  40679  paddasslem7  40701  paddasslem9  40703  paddasslem10  40704  paddasslem15  40709  poml6N  40830  osumcllem6N  40836  osumcllem7N  40837  pexmidlem4N  40848  pl42lem4N  40857  lhplt  40875  lhpjat1  40895  cdlemc5  41070  cdlemeg46fgN  41409  cdlemg12g  41524  tendoco2  41643  tendococl  41647  tendodi1  41659  tendoicl  41671  cdlemi2  41694  tendospdi1  41895  dihord11c  42099  dihmeetlem6  42184  dihjatc1  42186  dihmeetlem10N  42191  fltnltalem  43510  jm2.20nn  43840  kercvrlsm  43926  omord2lim  44143  frege96d  44591  frege98d  44595  ntrclsk3  44912  snunioo1  46344  limcleqr  46474  dvdivbd  46753  volioc  46802  iblspltprt  46803  volico  46813  stoweidlem1  46831  stoweidlem24  46854  etransclem23  47087  submodlt  48246  iccpartipre  48323  2pwp1prm  48494  perfectALTVlem2  48640  lincresunit2  49410  expnegico01  49450  itscnhlinecirc02plem3  49716