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  5107  funcnvtp  6582  fldiv  13829  digit2  14208  ccatass  14560  ccatpfx  14673  swrdswrd  14677  lcmfunsnlem2lem2  16616  cncongr1  16644  lsmval  19585  lsmelval  19586  lmimlbs  21752  mdetdiagid  22494  uncld  22935  hausnei2  23247  uptx  23519  xkohmeo  23709  cnextcn  23961  cnextfres1  23962  nmhmcn  25027  uniioombl  25497  dvcnvlem  25887  dvlip2  25907  taylply2  26282  dvtaylp  26285  taylthlem2  26289  taylthlem2OLD  26290  logbgcd1irr  26711  ftalem2  26991  gausslemma2dlem2  27285  ostth2lem3  27553  wlkeq  29569  eucrctshift  30179  numclwwlk1lem2foalem  30287  numclwlk1lem1  30305  ccatf1  32877  lindsadd  37614  prjspnfv01  42619  prjspner01  42620  omlimcl2  43238  naddwordnexlem3  43395  fmtnofac2lem  47573  uhgrimprop  47896  isubgr3stgr  47978  gpgnbgrvtx0  48069  gpgnbgrvtx1  48070  itsclc0xyqsolb  48763