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  6603  fldiv  14002  digit2  14382  ccatass  14736  ccatf1  14738  ccatpfx  14852  swrdswrd  14856  lcmfunsnlem2lem2  16816  cncongr1  16844  lsmval  19864  lsmelval  19865  lmimlbs  22144  mdetdiagid  22917  uncld  23361  hausnei2  23673  uptx  23946  xkohmeo  24136  cnextcn  24388  cnextfres1  24389  nmhmcn  25443  uniioombl  25912  dvcnvlem  26298  dvlip2  26317  taylply2  26697  dvtaylp  26699  taylthlem2  26703  logbgcd1irr  27124  ftalem2  27403  gausslemma2dlem2  27696  ostth2lem3  27964  wlkeq  30216  eucrctshift  30846  numclwwlk1lem2foalem  30954  numclwlk1lem1  30972  lindsadd  38627  lpssat  40161  lssatle  40163  omlimcl2  44335  naddwordnexlem3  44492  fmtnofac2lem  48744  uhgrimprop  49081  isubgr3stgr  49164  gpgnbgrvtx0  49263  gpgnbgrvtx1  49264  itsclc0xyqsolb  49973