Theorem syl2an2 589

Description: syl2an 287 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.)

Hypotheses

Ref	Expression
syl2an2.1	|- ( ph -> ps )
syl2an2.2	|- ( ( ch /\ ph ) -> th )
syl2an2.3	|- ( ( ps /\ th ) -> ta )

Assertion

Ref	Expression
syl2an2	|- ( ( ch /\ ph ) -> ta )

Proof of Theorem syl2an2

Step	Hyp	Ref	Expression
1		syl2an2.1	. . 3 |- ( ph -> ps )
2		syl2an2.2	. . 3 |- ( ( ch /\ ph ) -> th )
3		syl2an2.3	. . 3 |- ( ( ps /\ th ) -> ta )
4	1, 2, 3	syl2an 287	. 2 |- ( ( ph /\ ( ch /\ ph ) ) -> ta )
5	4	anabss7 578	1 |- ( ( ch /\ ph ) -> ta )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mapsnf1o  6715  xposdif  9839  qbtwnz  10208  seq3f1o  10460  exp3vallem  10477  fihashf1rn  10723  xrmin2inf  11231  sumrbdclem  11340  summodclem3  11343  zsumdc  11347  fsum3cvg2  11357  mertenslem2  11499  mertensabs  11500  prodrbdclem  11534  prodmodclem2a  11539  zproddc  11542  eftcl  11617  divalgmod  11886  gcdsupex  11912  gcdsupcl  11913  cncongr2  12058  isprm3  12072  eulerthlemrprm  12183  eulerthlema  12184  pcmptdvds  12297  lgsval2lem  13705  nninfself  14046