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  5086  funcnvtp  6540  fldiv  13756  digit2  14135  ccatass  14488  ccatpfx  14600  swrdswrd  14604  lcmfunsnlem2lem2  16542  cncongr1  16570  lsmval  19553  lsmelval  19554  lmimlbs  21766  mdetdiagid  22508  uncld  22949  hausnei2  23261  uptx  23533  xkohmeo  23723  cnextcn  23975  cnextfres1  23976  nmhmcn  25040  uniioombl  25510  dvcnvlem  25900  dvlip2  25920  taylply2  26295  dvtaylp  26298  taylthlem2  26302  taylthlem2OLD  26303  logbgcd1irr  26724  ftalem2  27004  gausslemma2dlem2  27298  ostth2lem3  27566  wlkeq  29605  eucrctshift  30213  numclwwlk1lem2foalem  30321  numclwlk1lem1  30339  ccatf1  32920  lindsadd  37632  prjspnfv01  42636  prjspner01  42637  omlimcl2  43254  naddwordnexlem3  43411  fmtnofac2lem  47578  uhgrimprop  47902  isubgr3stgr  47985  gpgnbgrvtx0  48084  gpgnbgrvtx1  48085  itsclc0xyqsolb  48781