Theorem syl2an3an 1418

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  syl2an23an  1419  disjxiun  5065  funcnvtp  6419  fldiv  13231  digit2  13600  ccatass  13944  ccatpfx  14065  swrdswrd  14069  lcmfunsnlem2lem2  15985  cncongr1  16013  lsmval  18775  lsmelval  18776  lmimlbs  20982  mdetdiagid  21211  uncld  21651  hausnei2  21963  uptx  22235  xkohmeo  22425  cnextcn  22677  cnextfres1  22678  nmhmcn  23726  uniioombl  24192  dvcnvlem  24575  dvlip2  24594  dvtaylp  24960  taylthlem2  24964  logbgcd1irr  25374  ftalem2  25653  gausslemma2dlem2  25945  ostth2lem3  26213  wlkeq  27417  eucrctshift  28024  numclwwlk1lem2foalem  28132  numclwlk1lem1  28150  ccatf1  30627  lindsadd  34887  fmtnofac2lem  43737  itsclc0xyqsolb  44764