Theorem syl2an2 602

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 589	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  7009  fcdmnn0fsuppg  9597  xposdif  10263  qbtwnz  10664  seq3f1o  10932  exp3vallem  10955  fihashf1rn  11205  fun2dmnop0  11280  xrmin2inf  12012  sumrbdclem  12122  summodclem3  12125  zsumdc  12129  fsum3cvg2  12139  mertenslem2  12281  mertensabs  12282  prodrbdclem  12316  prodmodclem2a  12321  zproddc  12324  eftcl  12399  divalgmod  12672  bitsmod  12701  gcdsupex  12712  gcdsupcl  12713  cncongr2  12860  isprm3  12874  eulerthlemrprm  12985  eulerthlema  12986  pcmptdvds  13102  prdsex  14149  elplyd  15765  ply1term  15767  lgsval2lem  16043  nninfself  16961