Theorem syl2an3an 1423

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 1420	1 ⊢ ((𝜑 ∧ 𝜃) → 𝜂)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  syl2an23an  1424  disjxiun  5146  funcnvtp  6612  fldiv  13825  digit2  14199  ccatass  14538  ccatpfx  14651  swrdswrd  14655  lcmfunsnlem2lem2  16576  cncongr1  16604  lsmval  19516  lsmelval  19517  lmimlbs  21391  mdetdiagid  22102  uncld  22545  hausnei2  22857  uptx  23129  xkohmeo  23319  cnextcn  23571  cnextfres1  23572  nmhmcn  24636  uniioombl  25106  dvcnvlem  25493  dvlip2  25512  dvtaylp  25882  taylthlem2  25886  logbgcd1irr  26299  ftalem2  26578  gausslemma2dlem2  26870  ostth2lem3  27138  wlkeq  28891  eucrctshift  29496  numclwwlk1lem2foalem  29604  numclwlk1lem1  29622  ccatf1  32115  lindsadd  36481  prjspnfv01  41366  prjspner01  41367  omlimcl2  41991  naddwordnexlem3  42150  fmtnofac2lem  46236  itsclc0xyqsolb  47456