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  6814  xposdif  9986  qbtwnz  10375  seq3f1o  10643  exp3vallem  10666  fihashf1rn  10914  xrmin2inf  11498  sumrbdclem  11607  summodclem3  11610  zsumdc  11614  fsum3cvg2  11624  mertenslem2  11766  mertensabs  11767  prodrbdclem  11801  prodmodclem2a  11806  zproddc  11809  eftcl  11884  divalgmod  12157  bitsmod  12186  gcdsupex  12197  gcdsupcl  12198  cncongr2  12345  isprm3  12359  eulerthlemrprm  12470  eulerthlema  12471  pcmptdvds  12587  prdsex  13019  elplyd  15131  ply1term  15133  lgsval2lem  15405  nninfself  15814