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  6805  xposdif  9976  qbtwnz  10360  seq3f1o  10628  exp3vallem  10651  fihashf1rn  10899  xrmin2inf  11452  sumrbdclem  11561  summodclem3  11564  zsumdc  11568  fsum3cvg2  11578  mertenslem2  11720  mertensabs  11721  prodrbdclem  11755  prodmodclem2a  11760  zproddc  11763  eftcl  11838  divalgmod  12111  bitsmod  12140  gcdsupex  12151  gcdsupcl  12152  cncongr2  12299  isprm3  12313  eulerthlemrprm  12424  eulerthlema  12425  pcmptdvds  12541  prdsex  12973  elplyd  15063  ply1term  15065  lgsval2lem  15337  nninfself  15746