Theorem syl2an2 594

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  6796  xposdif  9957  qbtwnz  10341  seq3f1o  10609  exp3vallem  10632  fihashf1rn  10880  xrmin2inf  11433  sumrbdclem  11542  summodclem3  11545  zsumdc  11549  fsum3cvg2  11559  mertenslem2  11701  mertensabs  11702  prodrbdclem  11736  prodmodclem2a  11741  zproddc  11744  eftcl  11819  divalgmod  12092  gcdsupex  12124  gcdsupcl  12125  cncongr2  12272  isprm3  12286  eulerthlemrprm  12397  eulerthlema  12398  pcmptdvds  12514  prdsex  12940  elplyd  14977  ply1term  14979  lgsval2lem  15251  nninfself  15657