Theorem syl2an3an 1430

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

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

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  syl2an23an  1431  disjxiun  5076  funcnvtp  6555  fldiv  13817  digit2  14196  ccatass  14549  ccatpfx  14661  swrdswrd  14665  lcmfunsnlem2lem2  16606  cncongr1  16634  lsmval  19621  lsmelval  19622  lmimlbs  21818  mdetdiagid  22590  uncld  23031  hausnei2  23343  uptx  23615  xkohmeo  23805  cnextcn  24057  cnextfres1  24058  nmhmcn  25112  uniioombl  25581  dvcnvlem  25968  dvlip2  25987  taylply2  26358  dvtaylp  26360  taylthlem2  26364  logbgcd1irr  26783  ftalem2  27062  gausslemma2dlem2  27355  ostth2lem3  27623  wlkeq  29727  eucrctshift  30338  numclwwlk1lem2foalem  30446  numclwlk1lem1  30464  ccatf1  33035  lindsadd  37981  lpssat  39506  lssatle  39508  prjspnfv01  43075  prjspner01  43076  omlimcl2  43688  naddwordnexlem3  43845  fmtnofac2lem  48047  uhgrimprop  48384  isubgr3stgr  48467  gpgnbgrvtx0  48566  gpgnbgrvtx1  48567  itsclc0xyqsolb  49262