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  6793  xposdif  9951  qbtwnz  10323  seq3f1o  10591  exp3vallem  10614  fihashf1rn  10862  xrmin2inf  11414  sumrbdclem  11523  summodclem3  11526  zsumdc  11530  fsum3cvg2  11540  mertenslem2  11682  mertensabs  11683  prodrbdclem  11717  prodmodclem2a  11722  zproddc  11725  eftcl  11800  divalgmod  12071  gcdsupex  12097  gcdsupcl  12098  cncongr2  12245  isprm3  12259  eulerthlemrprm  12370  eulerthlema  12371  pcmptdvds  12486  prdsex  12883  elplyd  14920  ply1term  14922  lgsval2lem  15167  nninfself  15573