Theorem syl2an2 871

Description: syl2an 493 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 493	. 2 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜑)) → 𝜏)
5	4	anabss7 858	1 ⊢ ((𝜒 ∧ 𝜑) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 196  df-an 385

This theorem is referenced by:  elrab3t  3330  reusv2lem3  4797  fvmpt2d  6202  fmptco  6303  fseqdom  8732  hashimarn  13085  divalgmod  14967  lcmfunsnlem2  15191  lcmflefac  15199  cncongr2  15220  esum2dlem  29481  bj-restsnss  32217  bj-restsnss2  32218  k0004lem3  37467  usgr1v  40482  cplgr2vpr  40655  vtxdg0e  40689  wlknewwlksn  41084  wwlksnextwrd  41103  wwlksnwwlksnon  41121  clwlkclwwlklem2a4  41206