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  6949  xposdif  10160  qbtwnz  10555  seq3f1o  10823  exp3vallem  10846  fihashf1rn  11094  fun2dmnop0  11158  xrmin2inf  11889  sumrbdclem  11999  summodclem3  12002  zsumdc  12006  fsum3cvg2  12016  mertenslem2  12158  mertensabs  12159  prodrbdclem  12193  prodmodclem2a  12198  zproddc  12201  eftcl  12276  divalgmod  12549  bitsmod  12578  gcdsupex  12589  gcdsupcl  12590  cncongr2  12737  isprm3  12751  eulerthlemrprm  12862  eulerthlema  12863  pcmptdvds  12979  prdsex  13413  elplyd  15532  ply1term  15534  lgsval2lem  15809  nninfself  16719