Theorem syl2an3an 1421

Description: syl3an 1159 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 1159	. 2 ⊢ ((𝜑 ∧ 𝜑 ∧ 𝜃) → 𝜂)
6	5	3anidm12 1418	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  1422  disjxiun  5145  funcnvtp  6631  fldiv  13897  digit2  14272  ccatass  14623  ccatpfx  14736  swrdswrd  14740  lcmfunsnlem2lem2  16673  cncongr1  16701  lsmval  19681  lsmelval  19682  lmimlbs  21874  mdetdiagid  22622  uncld  23065  hausnei2  23377  uptx  23649  xkohmeo  23839  cnextcn  24091  cnextfres1  24092  nmhmcn  25167  uniioombl  25638  dvcnvlem  26029  dvlip2  26049  taylply2  26424  dvtaylp  26427  taylthlem2  26431  taylthlem2OLD  26432  logbgcd1irr  26852  ftalem2  27132  gausslemma2dlem2  27426  ostth2lem3  27694  wlkeq  29667  eucrctshift  30272  numclwwlk1lem2foalem  30380  numclwlk1lem1  30398  ccatf1  32918  lindsadd  37600  prjspnfv01  42611  prjspner01  42612  omlimcl2  43231  naddwordnexlem3  43389  fmtnofac2lem  47493  isubgr3stgr  47878  gpgnbgrvtx0  47965  gpgnbgrvtx1  47966  itsclc0xyqsolb  48620