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  6972  fcdmnn0fsuppg  9551  xposdif  10215  qbtwnz  10611  seq3f1o  10879  exp3vallem  10902  fihashf1rn  11151  fun2dmnop0  11222  xrmin2inf  11953  sumrbdclem  12063  summodclem3  12066  zsumdc  12070  fsum3cvg2  12080  mertenslem2  12222  mertensabs  12223  prodrbdclem  12257  prodmodclem2a  12262  zproddc  12265  eftcl  12340  divalgmod  12613  bitsmod  12642  gcdsupex  12653  gcdsupcl  12654  cncongr2  12801  isprm3  12815  eulerthlemrprm  12926  eulerthlema  12927  pcmptdvds  13043  prdsex  13482  elplyd  15606  ply1term  15608  lgsval2lem  15883  nninfself  16791