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  6892  xposdif  10090  qbtwnz  10483  seq3f1o  10751  exp3vallem  10774  fihashf1rn  11022  fun2dmnop0  11082  xrmin2inf  11794  sumrbdclem  11903  summodclem3  11906  zsumdc  11910  fsum3cvg2  11920  mertenslem2  12062  mertensabs  12063  prodrbdclem  12097  prodmodclem2a  12102  zproddc  12105  eftcl  12180  divalgmod  12453  bitsmod  12482  gcdsupex  12493  gcdsupcl  12494  cncongr2  12641  isprm3  12655  eulerthlemrprm  12766  eulerthlema  12767  pcmptdvds  12883  prdsex  13317  elplyd  15430  ply1term  15432  lgsval2lem  15704  nninfself  16439