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  6552  fldiv  13774  digit2  14153  ccatass  14506  ccatpfx  14618  swrdswrd  14622  lcmfunsnlem2lem2  16560  cncongr1  16588  lsmval  19570  lsmelval  19571  lmimlbs  21783  mdetdiagid  22525  uncld  22966  hausnei2  23278  uptx  23550  xkohmeo  23740  cnextcn  23992  cnextfres1  23993  nmhmcn  25057  uniioombl  25527  dvcnvlem  25917  dvlip2  25937  taylply2  26312  dvtaylp  26315  taylthlem2  26319  taylthlem2OLD  26320  logbgcd1irr  26741  ftalem2  27021  gausslemma2dlem2  27315  ostth2lem3  27583  wlkeq  29623  eucrctshift  30234  numclwwlk1lem2foalem  30342  numclwlk1lem1  30360  ccatf1  32941  lindsadd  37663  lpssat  39122  lssatle  39124  prjspnfv01  42732  prjspner01  42733  omlimcl2  43349  naddwordnexlem3  43506  fmtnofac2lem  47682  uhgrimprop  48006  isubgr3stgr  48089  gpgnbgrvtx0  48188  gpgnbgrvtx1  48189  itsclc0xyqsolb  48885