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  6837  xposdif  10024  qbtwnz  10416  seq3f1o  10684  exp3vallem  10707  fihashf1rn  10955  fun2dmnop0  11014  xrmin2inf  11654  sumrbdclem  11763  summodclem3  11766  zsumdc  11770  fsum3cvg2  11780  mertenslem2  11922  mertensabs  11923  prodrbdclem  11957  prodmodclem2a  11962  zproddc  11965  eftcl  12040  divalgmod  12313  bitsmod  12342  gcdsupex  12353  gcdsupcl  12354  cncongr2  12501  isprm3  12515  eulerthlemrprm  12626  eulerthlema  12627  pcmptdvds  12743  prdsex  13176  elplyd  15288  ply1term  15290  lgsval2lem  15562  nninfself  16091