Theorem syl2an2 584

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 573	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  6703  xposdif  9818  qbtwnz  10187  seq3f1o  10439  exp3vallem  10456  fihashf1rn  10702  xrmin2inf  11209  sumrbdclem  11318  summodclem3  11321  zsumdc  11325  fsum3cvg2  11335  mertenslem2  11477  mertensabs  11478  prodrbdclem  11512  prodmodclem2a  11517  zproddc  11520  eftcl  11595  divalgmod  11864  gcdsupex  11890  gcdsupcl  11891  cncongr2  12036  isprm3  12050  eulerthlemrprm  12161  eulerthlema  12162  pcmptdvds  12275  lgsval2lem  13561  nninfself  13903