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  6971  fcdmnn0fsuppg  9547  xposdif  10211  qbtwnz  10607  seq3f1o  10875  exp3vallem  10898  fihashf1rn  11146  fun2dmnop0  11215  xrmin2inf  11946  sumrbdclem  12056  summodclem3  12059  zsumdc  12063  fsum3cvg2  12073  mertenslem2  12215  mertensabs  12216  prodrbdclem  12250  prodmodclem2a  12255  zproddc  12258  eftcl  12333  divalgmod  12606  bitsmod  12635  gcdsupex  12646  gcdsupcl  12647  cncongr2  12794  isprm3  12808  eulerthlemrprm  12919  eulerthlema  12920  pcmptdvds  13036  prdsex  13471  elplyd  15593  ply1term  15595  lgsval2lem  15870  nninfself  16778