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  6892  xposdif  10086  qbtwnz  10479  seq3f1o  10747  exp3vallem  10770  fihashf1rn  11018  fun2dmnop0  11077  xrmin2inf  11787  sumrbdclem  11896  summodclem3  11899  zsumdc  11903  fsum3cvg2  11913  mertenslem2  12055  mertensabs  12056  prodrbdclem  12090  prodmodclem2a  12095  zproddc  12098  eftcl  12173  divalgmod  12446  bitsmod  12475  gcdsupex  12486  gcdsupcl  12487  cncongr2  12634  isprm3  12648  eulerthlemrprm  12759  eulerthlema  12760  pcmptdvds  12876  prdsex  13310  elplyd  15423  ply1term  15425  lgsval2lem  15697  nninfself  16409