Theorem syl3an2 1233

Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)

Hypotheses

Ref	Expression
syl3an2.1	|- ( ph -> ch )
syl3an2.2	|- ( ( ps /\ ch /\ th ) -> ta )

Assertion

Ref	Expression
syl3an2	|- ( ( ps /\ ph /\ th ) -> ta )

Proof of Theorem syl3an2

Step	Hyp	Ref	Expression
1		syl3an2.1	. . 3 |- ( ph -> ch )
2		syl3an2.2	. . . 4 |- ( ( ps /\ ch /\ th ) -> ta )
3	2	3exp 1163	. . 3 |- ( ps -> ( ch -> ( th -> ta ) ) )
4	1, 3	syl5 32	. 2 |- ( ps -> ( ph -> ( th -> ta ) ) )
5	4	3imp 1158	1 |- ( ( ps /\ ph /\ th ) -> ta )

Syntax hints:   -> wi 4   /\ w3a 945

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 947

This theorem is referenced by:  syl3an2b  1236  syl3an2br  1239  syl3anl2  1248  nndi  6336  nnmass  6337  prarloclemarch2  7175  1idprl  7346  1idpru  7347  recexprlem1ssl  7389  recexprlem1ssu  7390  msqge0  8296  mulge0  8299  divsubdirap  8381  divdiv32ap  8393  peano2uz  9280  fzoshftral  9908  expdivap  10237  bcval5  10402  redivap  10539  imdivap  10546  absdiflt  10756  absdifle  10757  retanclap  11280  tannegap  11286  lcmgcdeq  11610  isprm3  11645  prmdvdsexpb  11673  cnpf2  12218  blres  12423