Theorem syl2an3an 1425

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 1422	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  1426  disjxiun  5096  funcnvtp  6556  fldiv  13784  digit2  14163  ccatass  14516  ccatpfx  14628  swrdswrd  14632  lcmfunsnlem2lem2  16570  cncongr1  16598  lsmval  19581  lsmelval  19582  lmimlbs  21795  mdetdiagid  22548  uncld  22989  hausnei2  23301  uptx  23573  xkohmeo  23763  cnextcn  24015  cnextfres1  24016  nmhmcn  25080  uniioombl  25550  dvcnvlem  25940  dvlip2  25960  taylply2  26335  dvtaylp  26338  taylthlem2  26342  taylthlem2OLD  26343  logbgcd1irr  26764  ftalem2  27044  gausslemma2dlem2  27338  ostth2lem3  27606  wlkeq  29690  eucrctshift  30301  numclwwlk1lem2foalem  30409  numclwlk1lem1  30427  ccatf1  33012  lindsadd  37785  lpssat  39310  lssatle  39312  prjspnfv01  42903  prjspner01  42904  omlimcl2  43520  naddwordnexlem3  43677  fmtnofac2lem  47850  uhgrimprop  48174  isubgr3stgr  48257  gpgnbgrvtx0  48356  gpgnbgrvtx1  48357  itsclc0xyqsolb  49052