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  6906  xposdif  10117  qbtwnz  10512  seq3f1o  10780  exp3vallem  10803  fihashf1rn  11051  fun2dmnop0  11115  xrmin2inf  11846  sumrbdclem  11956  summodclem3  11959  zsumdc  11963  fsum3cvg2  11973  mertenslem2  12115  mertensabs  12116  prodrbdclem  12150  prodmodclem2a  12155  zproddc  12158  eftcl  12233  divalgmod  12506  bitsmod  12535  gcdsupex  12546  gcdsupcl  12547  cncongr2  12694  isprm3  12708  eulerthlemrprm  12819  eulerthlema  12820  pcmptdvds  12936  prdsex  13370  elplyd  15484  ply1term  15486  lgsval2lem  15758  nninfself  16666