Theorem syl2an3an 1424

Description: syl3an 1160 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 1160	. 2 ⊢ ((𝜑 ∧ 𝜑 ∧ 𝜃) → 𝜂)
6	5	3anidm12 1421	1 ⊢ ((𝜑 ∧ 𝜃) → 𝜂)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  syl2an23an  1425  disjxiun  5104  funcnvtp  6579  fldiv  13822  digit2  14201  ccatass  14553  ccatpfx  14666  swrdswrd  14670  lcmfunsnlem2lem2  16609  cncongr1  16637  lsmval  19578  lsmelval  19579  lmimlbs  21745  mdetdiagid  22487  uncld  22928  hausnei2  23240  uptx  23512  xkohmeo  23702  cnextcn  23954  cnextfres1  23955  nmhmcn  25020  uniioombl  25490  dvcnvlem  25880  dvlip2  25900  taylply2  26275  dvtaylp  26278  taylthlem2  26282  taylthlem2OLD  26283  logbgcd1irr  26704  ftalem2  26984  gausslemma2dlem2  27278  ostth2lem3  27546  wlkeq  29562  eucrctshift  30172  numclwwlk1lem2foalem  30280  numclwlk1lem1  30298  ccatf1  32870  lindsadd  37607  prjspnfv01  42612  prjspner01  42613  omlimcl2  43231  naddwordnexlem3  43388  fmtnofac2lem  47569  uhgrimprop  47892  isubgr3stgr  47974  gpgnbgrvtx0  48065  gpgnbgrvtx1  48066  itsclc0xyqsolb  48759