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  6901  xposdif  10110  qbtwnz  10504  seq3f1o  10772  exp3vallem  10795  fihashf1rn  11043  fun2dmnop0  11104  xrmin2inf  11822  sumrbdclem  11931  summodclem3  11934  zsumdc  11938  fsum3cvg2  11948  mertenslem2  12090  mertensabs  12091  prodrbdclem  12125  prodmodclem2a  12130  zproddc  12133  eftcl  12208  divalgmod  12481  bitsmod  12510  gcdsupex  12521  gcdsupcl  12522  cncongr2  12669  isprm3  12683  eulerthlemrprm  12794  eulerthlema  12795  pcmptdvds  12911  prdsex  13345  elplyd  15458  ply1term  15460  lgsval2lem  15732  nninfself  16565