Theorem syl2an3an 1423

Description: syl3an 1161 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 1161	. 2 ⊢ ((𝜑 ∧ 𝜑 ∧ 𝜃) → 𝜂)
6	5	3anidm12 1420	1 ⊢ ((𝜑 ∧ 𝜃) → 𝜂)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1088

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 400  df-3an 1090

This theorem is referenced by:  syl2an23an  1424  disjxiun  5027  funcnvtp  6402  fldiv  13319  digit2  13689  ccatass  14031  ccatpfx  14152  swrdswrd  14156  lcmfunsnlem2lem2  16080  cncongr1  16108  lsmval  18891  lsmelval  18892  lmimlbs  20652  mdetdiagid  21351  uncld  21792  hausnei2  22104  uptx  22376  xkohmeo  22566  cnextcn  22818  cnextfres1  22819  nmhmcn  23872  uniioombl  24341  dvcnvlem  24728  dvlip2  24747  dvtaylp  25117  taylthlem2  25121  logbgcd1irr  25532  ftalem2  25811  gausslemma2dlem2  26103  ostth2lem3  26371  wlkeq  27575  eucrctshift  28180  numclwwlk1lem2foalem  28288  numclwlk1lem1  28306  ccatf1  30798  lindsadd  35393  prjspnfv01  40038  prjspner01  40039  fmtnofac2lem  44554  itsclc0xyqsolb  45650