Theorem syl2an3an 1445

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 401  df-3an 1103

This theorem is referenced by:  syl2an23an  1446  disjxiun  5102  funcnvtp  6588  fldiv  13884  digit2  14263  ccatass  14616  ccatpfx  14728  swrdswrd  14732  lcmfunsnlem2lem2  16687  cncongr1  16715  lsmval  19709  lsmelval  19710  lmimlbs  21946  mdetdiagid  22718  uncld  23159  hausnei2  23471  uptx  23743  xkohmeo  23933  cnextcn  24185  cnextfres1  24186  nmhmcn  25240  uniioombl  25709  dvcnvlem  26096  dvlip2  26115  taylply2  26489  dvtaylp  26491  taylthlem2  26495  logbgcd1irr  26917  ftalem2  27196  gausslemma2dlem2  27489  ostth2lem3  27757  wlkeq  29892  eucrctshift  30503  numclwwlk1lem2foalem  30611  numclwlk1lem1  30629  ccatf1  33182  lindsadd  38124  lpssat  39649  lssatle  39651  prjspnfv01  43218  prjspner01  43219  omlimcl2  43831  naddwordnexlem3  43988  fmtnofac2lem  48175  uhgrimprop  48512  isubgr3stgr  48595  gpgnbgrvtx0  48694  gpgnbgrvtx1  48695  itsclc0xyqsolb  49401