Theorem syl2an3an 1423

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 1090

This theorem is referenced by:  syl2an23an  1424  disjxiun  5145  funcnvtp  6609  fldiv  13822  digit2  14196  ccatass  14535  ccatpfx  14648  swrdswrd  14652  lcmfunsnlem2lem2  16573  cncongr1  16601  lsmval  19511  lsmelval  19512  lmimlbs  21383  mdetdiagid  22094  uncld  22537  hausnei2  22849  uptx  23121  xkohmeo  23311  cnextcn  23563  cnextfres1  23564  nmhmcn  24628  uniioombl  25098  dvcnvlem  25485  dvlip2  25504  dvtaylp  25874  taylthlem2  25878  logbgcd1irr  26289  ftalem2  26568  gausslemma2dlem2  26860  ostth2lem3  27128  wlkeq  28881  eucrctshift  29486  numclwwlk1lem2foalem  29594  numclwlk1lem1  29612  ccatf1  32103  lindsadd  36470  prjspnfv01  41363  prjspner01  41364  omlimcl2  41977  naddwordnexlem3  42136  fmtnofac2lem  46223  itsclc0xyqsolb  47410