Theorem syl2an2 598

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 585	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  6905  xposdif  10116  qbtwnz  10510  seq3f1o  10778  exp3vallem  10801  fihashf1rn  11049  fun2dmnop0  11110  xrmin2inf  11828  sumrbdclem  11937  summodclem3  11940  zsumdc  11944  fsum3cvg2  11954  mertenslem2  12096  mertensabs  12097  prodrbdclem  12131  prodmodclem2a  12136  zproddc  12139  eftcl  12214  divalgmod  12487  bitsmod  12516  gcdsupex  12527  gcdsupcl  12528  cncongr2  12675  isprm3  12689  eulerthlemrprm  12800  eulerthlema  12801  pcmptdvds  12917  prdsex  13351  elplyd  15464  ply1term  15466  lgsval2lem  15738  nninfself  16615