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  7025  xposdif  10300  qbtwnz  10702  seq3f1o  10974  exp3vallem  10997  fihashf1rn  11248  fun2dmnop0  11323  xrmin2inf  12058  sumrbdclem  12168  summodclem3  12171  zsumdc  12175  fsum3cvg2  12185  mertenslem2  12327  mertensabs  12328  prodrbdclem  12362  prodmodclem2a  12367  zproddc  12370  eftcl  12445  divalgmod  12718  bitsmod  12747  gcdsupex  12758  gcdsupcl  12759  cncongr2  12906  isprm3  12920  eulerthlemrprm  13035  eulerthlema  13036  pcmptdvds  13152  idjufi  14268  prdsex  14278  elplyd  15984  ply1term  15986  zprmlogbaplem3  16234  lgsval2lem  16351  nninfself  17279