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  7023  fcdmnn0fsuppg  9629  xposdif  10301  qbtwnz  10703  seq3f1o  10975  exp3vallem  10998  fihashf1rn  11249  fun2dmnop0  11324  xrmin2inf  12059  sumrbdclem  12169  summodclem3  12172  zsumdc  12176  fsum3cvg2  12186  mertenslem2  12328  mertensabs  12329  prodrbdclem  12363  prodmodclem2a  12368  zproddc  12371  eftcl  12446  divalgmod  12719  bitsmod  12748  gcdsupex  12759  gcdsupcl  12760  cncongr2  12907  isprm3  12921  eulerthlemrprm  13036  eulerthlema  13037  pcmptdvds  13153  idjufi  14269  prdsex  14279  elplyd  15967  ply1term  15969  zprmlogbaplem3  16217  lgsval2lem  16334  nninfself  17262