Theorem syl2an2 596

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  6882  xposdif  10074  qbtwnz  10466  seq3f1o  10734  exp3vallem  10757  fihashf1rn  11005  fun2dmnop0  11064  xrmin2inf  11774  sumrbdclem  11883  summodclem3  11886  zsumdc  11890  fsum3cvg2  11900  mertenslem2  12042  mertensabs  12043  prodrbdclem  12077  prodmodclem2a  12082  zproddc  12085  eftcl  12160  divalgmod  12433  bitsmod  12462  gcdsupex  12473  gcdsupcl  12474  cncongr2  12621  isprm3  12635  eulerthlemrprm  12746  eulerthlema  12747  pcmptdvds  12863  prdsex  13297  elplyd  15409  ply1term  15411  lgsval2lem  15683  nninfself  16338