Theorem syl2an2 602

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 589	1 ⊢ ((𝜒 ∧ 𝜑) → 𝜏)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  mapsnf1o  7019  fcdmnn0fsuppg  9620  xposdif  10286  qbtwnz  10688  seq3f1o  10956  exp3vallem  10979  fihashf1rn  11229  fun2dmnop0  11304  xrmin2inf  12036  sumrbdclem  12146  summodclem3  12149  zsumdc  12153  fsum3cvg2  12163  mertenslem2  12305  mertensabs  12306  prodrbdclem  12340  prodmodclem2a  12345  zproddc  12348  eftcl  12423  divalgmod  12696  bitsmod  12725  gcdsupex  12736  gcdsupcl  12737  cncongr2  12884  isprm3  12898  eulerthlemrprm  13009  eulerthlema  13010  pcmptdvds  13126  prdsex  14174  elplyd  15844  ply1term  15846  lgsval2lem  16141  nninfself  17068