Theorem syl2an2 594

Description: syl2an 289 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 289	. 2 |- ( ( ph /\ ( ch /\ ph ) ) -> ta )
5	4	anabss7 583	1 |- ( ( ch /\ ph ) -> ta )

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  6731  xposdif  9866  qbtwnz  10235  seq3f1o  10487  exp3vallem  10504  fihashf1rn  10749  xrmin2inf  11257  sumrbdclem  11366  summodclem3  11369  zsumdc  11373  fsum3cvg2  11383  mertenslem2  11525  mertensabs  11526  prodrbdclem  11560  prodmodclem2a  11565  zproddc  11568  eftcl  11643  divalgmod  11912  gcdsupex  11938  gcdsupcl  11939  cncongr2  12084  isprm3  12098  eulerthlemrprm  12209  eulerthlema  12210  pcmptdvds  12323  lgsval2lem  14071  nninfself  14411