Theorem syl2an2 602

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 589	1 |- ( ( ch /\ ph ) -> ta )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  mapsnf1o  7019  fcdmnn0fsuppg  9618  xposdif  10284  qbtwnz  10686  seq3f1o  10954  exp3vallem  10977  fihashf1rn  11227  fun2dmnop0  11302  xrmin2inf  12034  sumrbdclem  12144  summodclem3  12147  zsumdc  12151  fsum3cvg2  12161  mertenslem2  12303  mertensabs  12304  prodrbdclem  12338  prodmodclem2a  12343  zproddc  12346  eftcl  12421  divalgmod  12694  bitsmod  12723  gcdsupex  12734  gcdsupcl  12735  cncongr2  12882  isprm3  12896  eulerthlemrprm  13007  eulerthlema  13008  pcmptdvds  13124  prdsex  14172  elplyd  15842  ply1term  15844  lgsval2lem  16129  nninfself  17056