Theorem syl2an2 596

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 583	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  6897  xposdif  10095  qbtwnz  10488  seq3f1o  10756  exp3vallem  10779  fihashf1rn  11027  fun2dmnop0  11087  xrmin2inf  11800  sumrbdclem  11909  summodclem3  11912  zsumdc  11916  fsum3cvg2  11926  mertenslem2  12068  mertensabs  12069  prodrbdclem  12103  prodmodclem2a  12108  zproddc  12111  eftcl  12186  divalgmod  12459  bitsmod  12488  gcdsupex  12499  gcdsupcl  12500  cncongr2  12647  isprm3  12661  eulerthlemrprm  12772  eulerthlema  12773  pcmptdvds  12889  prdsex  13323  elplyd  15436  ply1term  15438  lgsval2lem  15710  nninfself  16493