Theorem syl2an2 910

Description: syl2an 495 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 495	. 2 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜑)) → 𝜏)
5	4	anabss7 897	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 197  df-an 385

This theorem is referenced by:  elrab3t  3504  reusv2lem3  5021  fvmpt2d  6457  fmptco  6561  fseqdom  9060  hashimarn  13440  divalgmod  15352  lcmfunsnlem2  15576  lcmflefac  15584  cncongr2  15605  usgr1v  26369  cplgr2vpr  26561  vtxdg0e  26602  wlknewwlksn  27018  wwlksnextwrd  27037  wwlksnwwlksnon  27055  wwlksnwwlksnonOLD  27057  clwlkclwwlklem2a4  27142  numclwwlk8  27582  esum2dlem  30485  fv1stcnv  32007  bj-restsnss  33361  bj-restsnss2  33362  k0004lem3  38968