Theorem syl32anc 1403

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 1398	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  9341  coftr  10256  fin1a2s  10397  ioounsn  13503  snunioo  13504  snunico  13505  snunioc  13506  leexp1ad  14212  exple1  14213  leexp2rd  14291  facubnd  14336  permnn  14362  sqgcd  16619  expgcd  16620  cncongr2  16725  prmdvdsbc  16784  hashgcdlem  16846  ramlb  17078  0ram  17079  ram0  17081  ramz2  17083  ramz  17084  ramcl  17088  lsmub1x  19715  lsmub2x  19716  lsmsubm  19722  pgpfac1lem2  20146  mptscmfsupp0  21027  2idlcpblrng  21389  xrsdsreclblem  21542  pzriprnglem12  21621  uvcff  21920  uvcresum  21922  frlmup1  21927  psrass1lem  22062  psrlidm  22090  psrridm  22091  psrcom  22096  mvrcl  22120  mplsubrglem  22132  mplcoe5  22170  mplbas2  22172  psrbagev1  22207  evlslem3  22210  evlslem6  22211  psropprmul  22376  evls1fpws  22508  smadiadetg  22809  cayhamlem4  23024  lecldbas  23355  pnfnei  23356  mnfnei  23357  clsconn  23566  txcls  23740  ufldom  24098  hauspwpwf1  24123  flfcnp  24140  flfcnp2  24143  cnpfcfi  24176  tsmsmhm  24282  met2ndci  24658  nghmco  24874  nghmplusg  24876  icopnfcld  24903  iocmnfcld  24904  tgioo  24932  reconnlem1  24963  metdseq0  24991  ovolunnul  25638  volinun  25684  volfiniun  25685  volsup  25694  icombl  25702  ioombl  25703  ovolioo  25706  ioorcl2  25710  volivth  25745  ismbf3d  25792  dvferm2lem  26124  lhop  26154  tayl0  26501  pserulm  26561  cxpcn3  26889  ssscongptld  26963  heron  26979  mpodvdsmulf1o  27334  dvdsmulf1o  27336  logexprlim  27365  perfectlem2  27370  lgssq  27477  lgssq2  27478  gausslemma2dlem7  27513  lgsquad2lem1  27524  lgsquad2lem2  27525  2sqblem  27571  addsq2nreurex  27584  ostth2lem2  27774  ostth3  27778  bdayfinbndlem1  28636  ubthlem2  31189  nmopleid  32457  elsuppfnd  32993  fsuppcurry1  33035  fsuppcurry2  33036  znumd  33123  zdend  33124  numdenneg  33125  mgcf1olem1  33287  mgcf1olem2  33288  gsummptres2  33339  archirngz  33475  archiabllem1a  33477  elrgspnlem2  33529  elrgspnlem3  33530  q1pdir  33859  q1pvsca  33860  ply1degltdimlem  33978  fedgmullem1  33985  fedgmullem2  33986  evls1fldgencl  34026  cos9thpiminplylem1  34138  cos9thpiminplylem2  34139  submatminr1  34166  locfinreflem  34196  sxbrsigalem2  34642  elmrsubrn  35978  ismblfin  38278  itg2gt0cn  38292  cntotbnd  38413  ismtyhmeolem  38421  heibor1lem  38426  heiborlem6  38433  rrnequiv  38452  1cvrat  40218  ps-2b  40224  2at0mat0  40267  ps-2c  40270  llncvrlpln2  40299  2llnmeqat  40313  4atlem10  40348  4atlem11a  40349  4atlem12a  40352  2lplnja  40361  dalemcea  40402  dalem2  40403  dalem21  40436  dalem54  40468  2lnat  40526  cdlemb  40536  elpaddat  40546  paddasslem7  40568  paddasslem9  40570  paddasslem10  40571  paddasslem15  40576  poml6N  40697  osumcllem6N  40703  osumcllem7N  40704  pexmidlem4N  40715  pl42lem4N  40724  lhplt  40742  lhpjat1  40762  cdlemc5  40937  cdlemeg46fgN  41276  cdlemg12g  41391  tendoco2  41510  tendococl  41514  tendodi1  41526  tendoicl  41538  cdlemi2  41561  tendospdi1  41762  dihord11c  41966  dihmeetlem6  42051  dihjatc1  42053  dihmeetlem10N  42058  fltnltalem  43364  jm2.20nn  43694  kercvrlsm  43780  omord2lim  43997  frege96d  44445  frege98d  44449  ntrclsk3  44766  snunioo1  46198  limcleqr  46328  dvdivbd  46607  volioc  46656  iblspltprt  46657  volico  46667  stoweidlem1  46685  stoweidlem24  46708  etransclem23  46941  submodlt  48060  iccpartipre  48137  2pwp1prm  48308  perfectALTVlem2  48454  lincresunit2  49225  expnegico01  49265  itscnhlinecirc02plem3  49531