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  5097  funcnvtp  6563  fldiv  13792  digit2  14171  ccatass  14524  ccatpfx  14636  swrdswrd  14640  lcmfunsnlem2lem2  16578  cncongr1  16606  lsmval  19589  lsmelval  19590  lmimlbs  21803  mdetdiagid  22556  uncld  22997  hausnei2  23309  uptx  23581  xkohmeo  23771  cnextcn  24023  cnextfres1  24024  nmhmcn  25088  uniioombl  25558  dvcnvlem  25948  dvlip2  25968  taylply2  26343  dvtaylp  26346  taylthlem2  26350  taylthlem2OLD  26351  logbgcd1irr  26772  ftalem2  27052  gausslemma2dlem2  27346  ostth2lem3  27614  wlkeq  29719  eucrctshift  30330  numclwwlk1lem2foalem  30438  numclwlk1lem1  30456  ccatf1  33041  lindsadd  37853  lpssat  39378  lssatle  39380  prjspnfv01  42971  prjspner01  42972  omlimcl2  43588  naddwordnexlem3  43745  fmtnofac2lem  47917  uhgrimprop  48241  isubgr3stgr  48324  gpgnbgrvtx0  48423  gpgnbgrvtx1  48424  itsclc0xyqsolb  49119