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  6751  xposdif  9896  qbtwnz  10266  seq3f1o  10518  exp3vallem  10535  fihashf1rn  10782  xrmin2inf  11290  sumrbdclem  11399  summodclem3  11402  zsumdc  11406  fsum3cvg2  11416  mertenslem2  11558  mertensabs  11559  prodrbdclem  11593  prodmodclem2a  11598  zproddc  11601  eftcl  11676  divalgmod  11946  gcdsupex  11972  gcdsupcl  11973  cncongr2  12118  isprm3  12132  eulerthlemrprm  12243  eulerthlema  12244  pcmptdvds  12357  prdsex  12736  lgsval2lem  14707  nninfself  15059