Theorem syl2an2 583

Description: syl2an 287 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 287	. 2 |- ( ( ph /\ ( ch /\ ph ) ) -> ta )
5	4	anabss7 572	1 |- ( ( ch /\ ph ) -> ta )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mapsnf1o  6631  xposdif  9665  qbtwnz  10029  seq3f1o  10277  exp3vallem  10294  fihashf1rn  10535  xrmin2inf  11037  sumrbdclem  11146  summodclem3  11149  zsumdc  11153  fsum3cvg2  11163  mertenslem2  11305  mertensabs  11306  prodrbdclem  11340  prodmodclem2a  11345  eftcl  11360  divalgmod  11624  gcdsupex  11646  gcdsupcl  11647  cncongr2  11785  isprm3  11799  nninfself  13209