Theorem syl2an2 602

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 589	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  7013  fcdmnn0fsuppg  9601  xposdif  10267  qbtwnz  10669  seq3f1o  10937  exp3vallem  10960  fihashf1rn  11210  fun2dmnop0  11285  xrmin2inf  12017  sumrbdclem  12127  summodclem3  12130  zsumdc  12134  fsum3cvg2  12144  mertenslem2  12286  mertensabs  12287  prodrbdclem  12321  prodmodclem2a  12326  zproddc  12329  eftcl  12404  divalgmod  12677  bitsmod  12706  gcdsupex  12717  gcdsupcl  12718  cncongr2  12865  isprm3  12879  eulerthlemrprm  12990  eulerthlema  12991  pcmptdvds  13107  prdsex  14155  elplyd  15825  ply1term  15827  lgsval2lem  16112  nninfself  17030