Theorem syl2an3an 1424

Description: syl3an 1160 with antecedents in standard conjunction form. (Contributed by Alan Sare, 31-Aug-2016.)

Hypotheses

Ref	Expression
syl2an3an.1	⊢ (𝜑 → 𝜓)
syl2an3an.2	⊢ (𝜑 → 𝜒)
syl2an3an.3	⊢ (𝜃 → 𝜏)
syl2an3an.4	⊢ ((𝜓 ∧ 𝜒 ∧ 𝜏) → 𝜂)

Assertion

Ref	Expression
syl2an3an	⊢ ((𝜑 ∧ 𝜃) → 𝜂)

Proof of Theorem syl2an3an

Step	Hyp	Ref	Expression
1		syl2an3an.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl2an3an.2	. . 3 ⊢ (𝜑 → 𝜒)
3		syl2an3an.3	. . 3 ⊢ (𝜃 → 𝜏)
4		syl2an3an.4	. . 3 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜏) → 𝜂)
5	1, 2, 3, 4	syl3an 1160	. 2 ⊢ ((𝜑 ∧ 𝜑 ∧ 𝜃) → 𝜂)
6	5	3anidm12 1421	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:  syl2an23an  1425  disjxiun  5121  funcnvtp  6604  fldiv  13882  digit2  14259  ccatass  14611  ccatpfx  14724  swrdswrd  14728  lcmfunsnlem2lem2  16663  cncongr1  16691  lsmval  19634  lsmelval  19635  lmimlbs  21801  mdetdiagid  22543  uncld  22984  hausnei2  23296  uptx  23568  xkohmeo  23758  cnextcn  24010  cnextfres1  24011  nmhmcn  25076  uniioombl  25547  dvcnvlem  25937  dvlip2  25957  taylply2  26332  dvtaylp  26335  taylthlem2  26339  taylthlem2OLD  26340  logbgcd1irr  26761  ftalem2  27041  gausslemma2dlem2  27335  ostth2lem3  27603  wlkeq  29619  eucrctshift  30229  numclwwlk1lem2foalem  30337  numclwlk1lem1  30355  ccatf1  32929  lindsadd  37642  prjspnfv01  42614  prjspner01  42615  omlimcl2  43233  naddwordnexlem3  43390  fmtnofac2lem  47549  uhgrimprop  47872  isubgr3stgr  47954  gpgnbgrvtx0  48043  gpgnbgrvtx1  48044  itsclc0xyqsolb  48717