Theorem syl2an3an 1449

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  syl2an23an  1450  disjxiun  5099  funcnvtp  6591  fldiv  13969  digit2  14348  ccatass  14702  ccatf1  14704  ccatpfx  14818  swrdswrd  14822  lcmfunsnlem2lem2  16777  cncongr1  16805  lsmval  19824  lsmelval  19825  lmimlbs  22104  mdetdiagid  22877  uncld  23321  hausnei2  23633  uptx  23906  xkohmeo  24096  cnextcn  24348  cnextfres1  24349  nmhmcn  25403  uniioombl  25872  dvcnvlem  26258  dvlip2  26277  taylply2  26659  dvtaylp  26661  taylthlem2  26665  logbgcd1irr  27086  ftalem2  27365  gausslemma2dlem2  27658  ostth2lem3  27926  wlkeq  30148  eucrctshift  30778  numclwwlk1lem2foalem  30886  numclwlk1lem1  30904  lindsadd  38456  lpssat  39990  lssatle  39992  prjspnfv01  43574  prjspner01  43575  omlimcl2  44187  naddwordnexlem3  44344  fmtnofac2lem  48575  uhgrimprop  48912  isubgr3stgr  48995  gpgnbgrvtx0  49094  gpgnbgrvtx1  49095  itsclc0xyqsolb  49804