Theorem syl2an3an 1425

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  syl2an23an  1426  disjxiun  5083  funcnvtp  6553  fldiv  13808  digit2  14187  ccatass  14540  ccatpfx  14652  swrdswrd  14656  lcmfunsnlem2lem2  16597  cncongr1  16625  lsmval  19612  lsmelval  19613  lmimlbs  21824  mdetdiagid  22574  uncld  23015  hausnei2  23327  uptx  23599  xkohmeo  23789  cnextcn  24041  cnextfres1  24042  nmhmcn  25096  uniioombl  25565  dvcnvlem  25952  dvlip2  25972  taylply2  26346  dvtaylp  26349  taylthlem2  26353  taylthlem2OLD  26354  logbgcd1irr  26775  ftalem2  27055  gausslemma2dlem2  27349  ostth2lem3  27617  wlkeq  29722  eucrctshift  30333  numclwwlk1lem2foalem  30441  numclwlk1lem1  30459  ccatf1  33029  lindsadd  37945  lpssat  39470  lssatle  39472  prjspnfv01  43068  prjspner01  43069  omlimcl2  43685  naddwordnexlem3  43842  fmtnofac2lem  48028  uhgrimprop  48365  isubgr3stgr  48448  gpgnbgrvtx0  48547  gpgnbgrvtx1  48548  itsclc0xyqsolb  49243