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  6739  xposdif  9884  qbtwnz  10254  seq3f1o  10506  exp3vallem  10523  fihashf1rn  10770  xrmin2inf  11278  sumrbdclem  11387  summodclem3  11390  zsumdc  11394  fsum3cvg2  11404  mertenslem2  11546  mertensabs  11547  prodrbdclem  11581  prodmodclem2a  11586  zproddc  11589  eftcl  11664  divalgmod  11934  gcdsupex  11960  gcdsupcl  11961  cncongr2  12106  isprm3  12120  eulerthlemrprm  12231  eulerthlema  12232  pcmptdvds  12345  prdsex  12723  lgsval2lem  14496  nninfself  14847