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  6911  xposdif  10122  qbtwnz  10517  seq3f1o  10785  exp3vallem  10808  fihashf1rn  11056  fun2dmnop0  11120  xrmin2inf  11851  sumrbdclem  11961  summodclem3  11964  zsumdc  11968  fsum3cvg2  11978  mertenslem2  12120  mertensabs  12121  prodrbdclem  12155  prodmodclem2a  12160  zproddc  12163  eftcl  12238  divalgmod  12511  bitsmod  12540  gcdsupex  12551  gcdsupcl  12552  cncongr2  12699  isprm3  12713  eulerthlemrprm  12824  eulerthlema  12825  pcmptdvds  12941  prdsex  13375  elplyd  15494  ply1term  15496  lgsval2lem  15768  nninfself  16678