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  5092  funcnvtp  6549  fldiv  13782  digit2  14161  ccatass  14513  ccatpfx  14625  swrdswrd  14629  lcmfunsnlem2lem2  16568  cncongr1  16596  lsmval  19545  lsmelval  19546  lmimlbs  21761  mdetdiagid  22503  uncld  22944  hausnei2  23256  uptx  23528  xkohmeo  23718  cnextcn  23970  cnextfres1  23971  nmhmcn  25036  uniioombl  25506  dvcnvlem  25896  dvlip2  25916  taylply2  26291  dvtaylp  26294  taylthlem2  26298  taylthlem2OLD  26299  logbgcd1irr  26720  ftalem2  27000  gausslemma2dlem2  27294  ostth2lem3  27562  wlkeq  29597  eucrctshift  30205  numclwwlk1lem2foalem  30313  numclwlk1lem1  30331  ccatf1  32903  lindsadd  37592  prjspnfv01  42597  prjspner01  42598  omlimcl2  43215  naddwordnexlem3  43372  fmtnofac2lem  47553  uhgrimprop  47876  isubgr3stgr  47958  gpgnbgrvtx0  48049  gpgnbgrvtx1  48050  itsclc0xyqsolb  48743