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  5111  funcnvtp  6606  fldiv  13913  digit2  14292  ccatass  14646  ccatf1  14648  ccatpfx  14762  swrdswrd  14766  lcmfunsnlem2lem2  16722  cncongr1  16750  lsmval  19743  lsmelval  19744  lmimlbs  22016  mdetdiagid  22787  uncld  23228  hausnei2  23540  uptx  23812  xkohmeo  24002  cnextcn  24254  cnextfres1  24255  nmhmcn  25309  uniioombl  25778  dvcnvlem  26165  dvlip2  26184  taylply2  26561  dvtaylp  26563  taylthlem2  26567  logbgcd1irr  26989  ftalem2  27268  gausslemma2dlem2  27561  ostth2lem3  27829  wlkeq  30013  eucrctshift  30624  numclwwlk1lem2foalem  30732  numclwlk1lem1  30750  lindsadd  38297  lpssat  39820  lssatle  39822  prjspnfv01  43389  prjspner01  43390  omlimcl2  44002  naddwordnexlem3  44159  fmtnofac2lem  48353  uhgrimprop  48690  isubgr3stgr  48773  gpgnbgrvtx0  48872  gpgnbgrvtx1  48873  itsclc0xyqsolb  49583