Theorem syl2an3an 1447

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  syl2an23an  1448  disjxiun  5105  funcnvtp  6599  fldiv  13893  digit2  14272  ccatass  14626  ccatpfx  14738  swrdswrd  14742  lcmfunsnlem2lem2  16696  cncongr1  16724  lsmval  19717  lsmelval  19718  lmimlbs  21965  mdetdiagid  22736  uncld  23177  hausnei2  23489  uptx  23761  xkohmeo  23951  cnextcn  24203  cnextfres1  24204  nmhmcn  25258  uniioombl  25727  dvcnvlem  26114  dvlip2  26133  taylply2  26507  dvtaylp  26509  taylthlem2  26513  logbgcd1irr  26935  ftalem2  27214  gausslemma2dlem2  27507  ostth2lem3  27775  wlkeq  29949  eucrctshift  30560  numclwwlk1lem2foalem  30668  numclwlk1lem1  30686  ccatf1  33235  lindsadd  38230  lpssat  39755  lssatle  39757  prjspnfv01  43326  prjspner01  43327  omlimcl2  43939  naddwordnexlem3  44096  fmtnofac2lem  48287  uhgrimprop  48624  isubgr3stgr  48707  gpgnbgrvtx0  48806  gpgnbgrvtx1  48807  itsclc0xyqsolb  49517