Theorem syl2an2 596

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  6901  xposdif  10107  qbtwnz  10501  seq3f1o  10769  exp3vallem  10792  fihashf1rn  11040  fun2dmnop0  11101  xrmin2inf  11819  sumrbdclem  11928  summodclem3  11931  zsumdc  11935  fsum3cvg2  11945  mertenslem2  12087  mertensabs  12088  prodrbdclem  12122  prodmodclem2a  12127  zproddc  12130  eftcl  12205  divalgmod  12478  bitsmod  12507  gcdsupex  12518  gcdsupcl  12519  cncongr2  12666  isprm3  12680  eulerthlemrprm  12791  eulerthlema  12792  pcmptdvds  12908  prdsex  13342  elplyd  15455  ply1term  15457  lgsval2lem  15729  nninfself  16551