Theorem syl2an2 598

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 585	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  6906  xposdif  10117  qbtwnz  10512  seq3f1o  10780  exp3vallem  10803  fihashf1rn  11051  fun2dmnop0  11112  xrmin2inf  11830  sumrbdclem  11940  summodclem3  11943  zsumdc  11947  fsum3cvg2  11957  mertenslem2  12099  mertensabs  12100  prodrbdclem  12134  prodmodclem2a  12139  zproddc  12142  eftcl  12217  divalgmod  12490  bitsmod  12519  gcdsupex  12530  gcdsupcl  12531  cncongr2  12678  isprm3  12692  eulerthlemrprm  12803  eulerthlema  12804  pcmptdvds  12920  prdsex  13354  elplyd  15468  ply1term  15470  lgsval2lem  15742  nninfself  16636