Theorem syl2an2 594

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  6805  xposdif  9974  qbtwnz  10358  seq3f1o  10626  exp3vallem  10649  fihashf1rn  10897  xrmin2inf  11450  sumrbdclem  11559  summodclem3  11562  zsumdc  11566  fsum3cvg2  11576  mertenslem2  11718  mertensabs  11719  prodrbdclem  11753  prodmodclem2a  11758  zproddc  11761  eftcl  11836  divalgmod  12109  bitsmod  12138  gcdsupex  12149  gcdsupcl  12150  cncongr2  12297  isprm3  12311  eulerthlemrprm  12422  eulerthlema  12423  pcmptdvds  12539  prdsex  12971  elplyd  15061  ply1term  15063  lgsval2lem  15335  nninfself  15744