Theorem syl2an3an 1449

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  syl2an23an  1450  disjxiun  5104  funcnvtp  6600  fldiv  13925  digit2  14304  ccatass  14658  ccatf1  14660  ccatpfx  14774  swrdswrd  14778  lcmfunsnlem2lem2  16735  cncongr1  16763  lsmval  19781  lsmelval  19782  lmimlbs  22055  mdetdiagid  22828  uncld  23272  hausnei2  23584  uptx  23857  xkohmeo  24047  cnextcn  24299  cnextfres1  24300  nmhmcn  25354  uniioombl  25823  dvcnvlem  26210  dvlip2  26229  taylply2  26611  dvtaylp  26613  taylthlem2  26617  logbgcd1irr  27039  ftalem2  27318  gausslemma2dlem2  27611  ostth2lem3  27879  wlkeq  30101  eucrctshift  30731  numclwwlk1lem2foalem  30839  numclwlk1lem1  30857  lindsadd  38375  lpssat  39894  lssatle  39896  prjspnfv01  43478  prjspner01  43479  omlimcl2  44091  naddwordnexlem3  44248  fmtnofac2lem  48479  uhgrimprop  48816  isubgr3stgr  48899  gpgnbgrvtx0  48998  gpgnbgrvtx1  48999  itsclc0xyqsolb  49708