Theorem syl2an3an 1424

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 1421	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  1425  disjxiun  5140  funcnvtp  6629  fldiv  13900  digit2  14275  ccatass  14626  ccatpfx  14739  swrdswrd  14743  lcmfunsnlem2lem2  16676  cncongr1  16704  lsmval  19666  lsmelval  19667  lmimlbs  21856  mdetdiagid  22606  uncld  23049  hausnei2  23361  uptx  23633  xkohmeo  23823  cnextcn  24075  cnextfres1  24076  nmhmcn  25153  uniioombl  25624  dvcnvlem  26014  dvlip2  26034  taylply2  26409  dvtaylp  26412  taylthlem2  26416  taylthlem2OLD  26417  logbgcd1irr  26837  ftalem2  27117  gausslemma2dlem2  27411  ostth2lem3  27679  wlkeq  29652  eucrctshift  30262  numclwwlk1lem2foalem  30370  numclwlk1lem1  30388  ccatf1  32933  lindsadd  37620  prjspnfv01  42634  prjspner01  42635  omlimcl2  43254  naddwordnexlem3  43412  fmtnofac2lem  47555  isubgr3stgr  47942  gpgnbgrvtx0  48030  gpgnbgrvtx1  48031  itsclc0xyqsolb  48691