Theorem syl2an3an 1422

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 1419	1 ⊢ ((𝜑 ∧ 𝜃) → 𝜂)

Syntax hints:   → wi 4   ∧ wa 397   ∧ 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 206  df-an 398  df-3an 1089

This theorem is referenced by:  syl2an23an  1423  disjxiun  5078  funcnvtp  6526  fldiv  13630  digit2  14001  ccatass  14342  ccatpfx  14463  swrdswrd  14467  lcmfunsnlem2lem2  16393  cncongr1  16421  lsmval  19302  lsmelval  19303  lmimlbs  21092  mdetdiagid  21798  uncld  22241  hausnei2  22553  uptx  22825  xkohmeo  23015  cnextcn  23267  cnextfres1  23268  nmhmcn  24332  uniioombl  24802  dvcnvlem  25189  dvlip2  25208  dvtaylp  25578  taylthlem2  25582  logbgcd1irr  25993  ftalem2  26272  gausslemma2dlem2  26564  ostth2lem3  26832  wlkeq  28050  eucrctshift  28656  numclwwlk1lem2foalem  28764  numclwlk1lem1  28782  ccatf1  31272  lindsadd  35818  prjspnfv01  40656  prjspner01  40657  fmtnofac2lem  45264  itsclc0xyqsolb  46360