Theorem syl2an2 598

Description: syl2an 289 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.)

Hypotheses

Ref	Expression
syl2an2.1	⊢ (𝜑 → 𝜓)
syl2an2.2	⊢ ((𝜒 ∧ 𝜑) → 𝜃)
syl2an2.3	⊢ ((𝜓 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
syl2an2	⊢ ((𝜒 ∧ 𝜑) → 𝜏)

Proof of Theorem syl2an2

Step	Hyp	Ref	Expression
1		syl2an2.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl2an2.2	. . 3 ⊢ ((𝜒 ∧ 𝜑) → 𝜃)
3		syl2an2.3	. . 3 ⊢ ((𝜓 ∧ 𝜃) → 𝜏)
4	1, 2, 3	syl2an 289	. 2 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜑)) → 𝜏)
5	4	anabss7 585	1 ⊢ ((𝜒 ∧ 𝜑) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mapsnf1o  6985  fcdmnn0fsuppg  9571  xposdif  10237  qbtwnz  10638  seq3f1o  10906  exp3vallem  10929  fihashf1rn  11179  fun2dmnop0  11250  xrmin2inf  11981  sumrbdclem  12091  summodclem3  12094  zsumdc  12098  fsum3cvg2  12108  mertenslem2  12250  mertensabs  12251  prodrbdclem  12285  prodmodclem2a  12290  zproddc  12293  eftcl  12368  divalgmod  12641  bitsmod  12670  gcdsupex  12681  gcdsupcl  12682  cncongr2  12829  isprm3  12843  eulerthlemrprm  12954  eulerthlema  12955  pcmptdvds  13071  prdsex  14117  elplyd  15735  ply1term  15737  lgsval2lem  16012  nninfself  16930