Theorem syl2an3an 1420

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

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

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 396  df-3an 1087

This theorem is referenced by:  syl2an23an  1421  disjxiun  5075  funcnvtp  6493  fldiv  13561  digit2  13932  ccatass  14274  ccatpfx  14395  swrdswrd  14399  lcmfunsnlem2lem2  16325  cncongr1  16353  lsmval  19234  lsmelval  19235  lmimlbs  21024  mdetdiagid  21730  uncld  22173  hausnei2  22485  uptx  22757  xkohmeo  22947  cnextcn  23199  cnextfres1  23200  nmhmcn  24264  uniioombl  24734  dvcnvlem  25121  dvlip2  25140  dvtaylp  25510  taylthlem2  25514  logbgcd1irr  25925  ftalem2  26204  gausslemma2dlem2  26496  ostth2lem3  26764  wlkeq  27981  eucrctshift  28586  numclwwlk1lem2foalem  28694  numclwlk1lem1  28712  ccatf1  31202  lindsadd  35749  prjspnfv01  40441  prjspner01  40442  fmtnofac2lem  44972  itsclc0xyqsolb  46068