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 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  1423  disjxiun  5163  funcnvtp  6641  fldiv  13911  digit2  14285  ccatass  14636  ccatpfx  14749  swrdswrd  14753  lcmfunsnlem2lem2  16686  cncongr1  16714  lsmval  19690  lsmelval  19691  lmimlbs  21879  mdetdiagid  22627  uncld  23070  hausnei2  23382  uptx  23654  xkohmeo  23844  cnextcn  24096  cnextfres1  24097  nmhmcn  25172  uniioombl  25643  dvcnvlem  26034  dvlip2  26054  taylply2  26427  dvtaylp  26430  taylthlem2  26434  taylthlem2OLD  26435  logbgcd1irr  26855  ftalem2  27135  gausslemma2dlem2  27429  ostth2lem3  27697  wlkeq  29670  eucrctshift  30275  numclwwlk1lem2foalem  30383  numclwlk1lem1  30401  ccatf1  32915  lindsadd  37573  prjspnfv01  42579  prjspner01  42580  omlimcl2  43203  naddwordnexlem3  43361  fmtnofac2lem  47442  itsclc0xyqsolb  48504