Theorem syl2an2 875

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  elrab3t  3362  reusv2lem3  4871  fvmpt2d  6293  fmptco  6396  fseqdom  8849  hashimarn  13227  divalgmod  15129  lcmfunsnlem2  15353  lcmflefac  15361  cncongr2  15382  usgr1v  26148  cplgr2vpr  26329  vtxdg0e  26370  wlknewwlksn  26773  wwlksnextwrd  26792  wwlksnwwlksnon  26810  clwlkclwwlklem2a4  26898  esum2dlem  30154  fv1stcnv  31680  bj-restsnss  33036  bj-restsnss2  33037  k0004lem3  38447