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  6985  fcdmnn0fsuppg  9568  xposdif  10234  qbtwnz  10635  seq3f1o  10903  exp3vallem  10926  fihashf1rn  11176  fun2dmnop0  11247  xrmin2inf  11978  sumrbdclem  12088  summodclem3  12091  zsumdc  12095  fsum3cvg2  12105  mertenslem2  12247  mertensabs  12248  prodrbdclem  12282  prodmodclem2a  12287  zproddc  12290  eftcl  12365  divalgmod  12638  bitsmod  12667  gcdsupex  12678  gcdsupcl  12679  cncongr2  12826  isprm3  12840  eulerthlemrprm  12951  eulerthlema  12952  pcmptdvds  13068  prdsex  14114  elplyd  15732  ply1term  15734  lgsval2lem  16009  nninfself  16917