Theorem syl2an3an 1425

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  syl2an23an  1426  disjxiun  5083  funcnvtp  6562  fldiv  13819  digit2  14198  ccatass  14551  ccatpfx  14663  swrdswrd  14667  lcmfunsnlem2lem2  16608  cncongr1  16636  lsmval  19623  lsmelval  19624  lmimlbs  21816  mdetdiagid  22565  uncld  23006  hausnei2  23318  uptx  23590  xkohmeo  23780  cnextcn  24032  cnextfres1  24033  nmhmcn  25087  uniioombl  25556  dvcnvlem  25943  dvlip2  25962  taylply2  26333  dvtaylp  26335  taylthlem2  26339  logbgcd1irr  26758  ftalem2  27037  gausslemma2dlem2  27330  ostth2lem3  27598  wlkeq  29702  eucrctshift  30313  numclwwlk1lem2foalem  30421  numclwlk1lem1  30439  ccatf1  33009  lindsadd  37934  lpssat  39459  lssatle  39461  prjspnfv01  43057  prjspner01  43058  omlimcl2  43670  naddwordnexlem3  43827  fmtnofac2lem  48025  uhgrimprop  48362  isubgr3stgr  48445  gpgnbgrvtx0  48544  gpgnbgrvtx1  48545  itsclc0xyqsolb  49240