Theorem syl2an2 594

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  6823  xposdif  10003  qbtwnz  10392  seq3f1o  10660  exp3vallem  10683  fihashf1rn  10931  fun2dmnop0  10990  xrmin2inf  11550  sumrbdclem  11659  summodclem3  11662  zsumdc  11666  fsum3cvg2  11676  mertenslem2  11818  mertensabs  11819  prodrbdclem  11853  prodmodclem2a  11858  zproddc  11861  eftcl  11936  divalgmod  12209  bitsmod  12238  gcdsupex  12249  gcdsupcl  12250  cncongr2  12397  isprm3  12411  eulerthlemrprm  12522  eulerthlema  12523  pcmptdvds  12639  prdsex  13072  elplyd  15184  ply1term  15186  lgsval2lem  15458  nninfself  15912