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 396   ∧ 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 397  df-3an 1089

This theorem is referenced by:  syl2an23an  1423  disjxiun  5145  funcnvtp  6611  fldiv  13827  digit2  14201  ccatass  14540  ccatpfx  14653  swrdswrd  14657  lcmfunsnlem2lem2  16578  cncongr1  16606  lsmval  19518  lsmelval  19519  lmimlbs  21397  mdetdiagid  22109  uncld  22552  hausnei2  22864  uptx  23136  xkohmeo  23326  cnextcn  23578  cnextfres1  23579  nmhmcn  24643  uniioombl  25113  dvcnvlem  25500  dvlip2  25519  dvtaylp  25889  taylthlem2  25893  logbgcd1irr  26306  ftalem2  26585  gausslemma2dlem2  26877  ostth2lem3  27145  wlkeq  28929  eucrctshift  29534  numclwwlk1lem2foalem  29642  numclwlk1lem1  29660  ccatf1  32153  lindsadd  36567  prjspnfv01  41448  prjspner01  41449  omlimcl2  42073  naddwordnexlem3  42232  fmtnofac2lem  46315  itsclc0xyqsolb  47534