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  6797  xposdif  9959  qbtwnz  10343  seq3f1o  10611  exp3vallem  10634  fihashf1rn  10882  xrmin2inf  11435  sumrbdclem  11544  summodclem3  11547  zsumdc  11551  fsum3cvg2  11561  mertenslem2  11703  mertensabs  11704  prodrbdclem  11738  prodmodclem2a  11743  zproddc  11746  eftcl  11821  divalgmod  12094  bitsmod  12123  gcdsupex  12134  gcdsupcl  12135  cncongr2  12282  isprm3  12296  eulerthlemrprm  12407  eulerthlema  12408  pcmptdvds  12524  prdsex  12950  elplyd  14987  ply1term  14989  lgsval2lem  15261  nninfself  15667