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  6854  xposdif  10046  qbtwnz  10438  seq3f1o  10706  exp3vallem  10729  fihashf1rn  10977  fun2dmnop0  11036  xrmin2inf  11745  sumrbdclem  11854  summodclem3  11857  zsumdc  11861  fsum3cvg2  11871  mertenslem2  12013  mertensabs  12014  prodrbdclem  12048  prodmodclem2a  12053  zproddc  12056  eftcl  12131  divalgmod  12404  bitsmod  12433  gcdsupex  12444  gcdsupcl  12445  cncongr2  12592  isprm3  12606  eulerthlemrprm  12717  eulerthlema  12718  pcmptdvds  12834  prdsex  13268  elplyd  15380  ply1term  15382  lgsval2lem  15654  nninfself  16290