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  6791  xposdif  9948  qbtwnz  10320  seq3f1o  10588  exp3vallem  10611  fihashf1rn  10859  xrmin2inf  11411  sumrbdclem  11520  summodclem3  11523  zsumdc  11527  fsum3cvg2  11537  mertenslem2  11679  mertensabs  11680  prodrbdclem  11714  prodmodclem2a  11719  zproddc  11722  eftcl  11797  divalgmod  12068  gcdsupex  12094  gcdsupcl  12095  cncongr2  12242  isprm3  12256  eulerthlemrprm  12367  eulerthlema  12368  pcmptdvds  12483  prdsex  12880  elplyd  14887  ply1term  14889  lgsval2lem  15126  nninfself  15503