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  9622  xposdif  10294  qbtwnz  10696  seq3f1o  10967  exp3vallem  10990  fihashf1rn  11241  fun2dmnop0  11316  xrmin2inf  12050  sumrbdclem  12160  summodclem3  12163  zsumdc  12167  fsum3cvg2  12177  mertenslem2  12319  mertensabs  12320  prodrbdclem  12354  prodmodclem2a  12359  zproddc  12362  eftcl  12437  divalgmod  12710  bitsmod  12739  gcdsupex  12750  gcdsupcl  12751  cncongr2  12898  isprm3  12912  eulerthlemrprm  13027  eulerthlema  13028  pcmptdvds  13144  prdsex  14221  elplyd  15891  ply1term  15893  zprmlogbaplem3  16136  lgsval2lem  16227  nninfself  17154