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  6831  xposdif  10011  qbtwnz  10401  seq3f1o  10669  exp3vallem  10692  fihashf1rn  10940  fun2dmnop0  10999  xrmin2inf  11623  sumrbdclem  11732  summodclem3  11735  zsumdc  11739  fsum3cvg2  11749  mertenslem2  11891  mertensabs  11892  prodrbdclem  11926  prodmodclem2a  11931  zproddc  11934  eftcl  12009  divalgmod  12282  bitsmod  12311  gcdsupex  12322  gcdsupcl  12323  cncongr2  12470  isprm3  12484  eulerthlemrprm  12595  eulerthlema  12596  pcmptdvds  12712  prdsex  13145  elplyd  15257  ply1term  15259  lgsval2lem  15531  nninfself  16024