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  9623  xposdif  10295  qbtwnz  10697  seq3f1o  10969  exp3vallem  10992  fihashf1rn  11243  fun2dmnop0  11318  xrmin2inf  12053  sumrbdclem  12163  summodclem3  12166  zsumdc  12170  fsum3cvg2  12180  mertenslem2  12322  mertensabs  12323  prodrbdclem  12357  prodmodclem2a  12362  zproddc  12365  eftcl  12440  divalgmod  12713  bitsmod  12742  gcdsupex  12753  gcdsupcl  12754  cncongr2  12901  isprm3  12915  eulerthlemrprm  13030  eulerthlema  13031  pcmptdvds  13147  prdsex  14224  elplyd  15895  ply1term  15897  zprmlogbaplem3  16140  lgsval2lem  16257  nninfself  17184