Theorem syl2an3an 1422

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 1419	1 ⊢ ((𝜑 ∧ 𝜃) → 𝜂)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  syl2an23an  1423  disjxiun  5107  funcnvtp  6569  fldiv  13775  digit2  14149  ccatass  14488  ccatpfx  14601  swrdswrd  14605  lcmfunsnlem2lem2  16526  cncongr1  16554  lsmval  19444  lsmelval  19445  lmimlbs  21279  mdetdiagid  21986  uncld  22429  hausnei2  22741  uptx  23013  xkohmeo  23203  cnextcn  23455  cnextfres1  23456  nmhmcn  24520  uniioombl  24990  dvcnvlem  25377  dvlip2  25396  dvtaylp  25766  taylthlem2  25770  logbgcd1irr  26181  ftalem2  26460  gausslemma2dlem2  26752  ostth2lem3  27020  wlkeq  28645  eucrctshift  29250  numclwwlk1lem2foalem  29358  numclwlk1lem1  29376  ccatf1  31875  lindsadd  36144  prjspnfv01  41020  prjspner01  41021  omlimcl2  41634  naddwordnexlem3  41793  fmtnofac2lem  45880  itsclc0xyqsolb  46976