Theorem syl2an3an 1437

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1095

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 209  df-an 399  df-3an 1097

This theorem is referenced by:  syl2an23an  1438  disjxiun  5091  funcnvtp  6573  fldiv  13860  digit2  14239  ccatass  14592  ccatpfx  14704  swrdswrd  14708  lcmfunsnlem2lem2  16649  cncongr1  16677  lsmval  19664  lsmelval  19665  lmimlbs  21861  mdetdiagid  22633  uncld  23074  hausnei2  23386  uptx  23658  xkohmeo  23848  cnextcn  24100  cnextfres1  24101  nmhmcn  25155  uniioombl  25624  dvcnvlem  26011  dvlip2  26030  taylply2  26401  dvtaylp  26403  taylthlem2  26407  logbgcd1irr  26829  ftalem2  27108  gausslemma2dlem2  27401  ostth2lem3  27669  wlkeq  29773  eucrctshift  30384  numclwwlk1lem2foalem  30492  numclwlk1lem1  30510  ccatf1  33081  lindsadd  38060  lpssat  39585  lssatle  39587  prjspnfv01  43154  prjspner01  43155  omlimcl2  43767  naddwordnexlem3  43924  fmtnofac2lem  48125  uhgrimprop  48462  isubgr3stgr  48545  gpgnbgrvtx0  48644  gpgnbgrvtx1  48645  itsclc0xyqsolb  49340