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  6949  xposdif  10161  qbtwnz  10557  seq3f1o  10825  exp3vallem  10848  fihashf1rn  11096  fun2dmnop0  11160  xrmin2inf  11891  sumrbdclem  12001  summodclem3  12004  zsumdc  12008  fsum3cvg2  12018  mertenslem2  12160  mertensabs  12161  prodrbdclem  12195  prodmodclem2a  12200  zproddc  12203  eftcl  12278  divalgmod  12551  bitsmod  12580  gcdsupex  12591  gcdsupcl  12592  cncongr2  12739  isprm3  12753  eulerthlemrprm  12864  eulerthlema  12865  pcmptdvds  12981  prdsex  13415  elplyd  15535  ply1term  15537  lgsval2lem  15812  nninfself  16722