Theorem syl2an3an 1450

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 1447	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  1451  disjxiun  5103  funcnvtp  6625  fldiv  14027  digit2  14407  ccatass  14761  ccatf1  14763  ccatpfx  14878  swrdswrd  14882  lcmfunsnlem2lem2  16843  cncongr1  16871  lsmval  19892  lsmelval  19893  lmimlbs  22172  mdetdiagid  22945  uncld  23389  hausnei2  23701  uptx  23974  xkohmeo  24164  cnextcn  24416  cnextfres1  24417  nmhmcn  25471  uniioombl  25940  dvcnvlem  26326  dvlip2  26345  taylply2  26725  dvtaylp  26727  taylthlem2  26731  logbgcd1irr  27152  ftalem2  27431  gausslemma2dlem2  27724  ostth2lem3  27992  wlkeq  30244  eucrctshift  30874  numclwwlk1lem2foalem  30982  numclwlk1lem1  31000  lindsadd  38728  lpssat  40262  lssatle  40264  omlimcl2  44436  naddwordnexlem3  44593  fmtnofac2lem  48858  uhgrimprop  49195  isubgr3stgr  49278  gpgnbgrvtx0  49377  gpgnbgrvtx1  49378  itsclc0xyqsolb  50087