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  6974  fcdmnn0fsuppg  9556  xposdif  10221  qbtwnz  10618  seq3f1o  10886  exp3vallem  10909  fihashf1rn  11159  fun2dmnop0  11230  xrmin2inf  11961  sumrbdclem  12071  summodclem3  12074  zsumdc  12078  fsum3cvg2  12088  mertenslem2  12230  mertensabs  12231  prodrbdclem  12265  prodmodclem2a  12270  zproddc  12273  eftcl  12348  divalgmod  12621  bitsmod  12650  gcdsupex  12661  gcdsupcl  12662  cncongr2  12809  isprm3  12823  eulerthlemrprm  12934  eulerthlema  12935  pcmptdvds  13051  prdsex  13503  elplyd  15655  ply1term  15657  lgsval2lem  15932  nninfself  16840