Theorem syl3an2 1272

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 1202	. . 3 |- ( ps -> ( ch -> ( th -> ta ) ) )
4	1, 3	syl5 32	. 2 |- ( ps -> ( ph -> ( th -> ta ) ) )
5	4	3imp 1193	1 |- ( ( ps /\ ph /\ th ) -> ta )

Syntax hints:   -> wi 4   /\ w3a 978

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  df-3an 980

This theorem is referenced by:  syl3an2b  1275  syl3an2br  1278  syl3anl2  1287  nndi  6489  nnmass  6490  prarloclemarch2  7420  1idprl  7591  1idpru  7592  recexprlem1ssl  7634  recexprlem1ssu  7635  msqge0  8575  mulge0  8578  divsubdirap  8667  divdiv32ap  8679  peano2uz  9585  fzoshftral  10240  expdivap  10573  bcval5  10745  redivap  10885  imdivap  10892  absdiflt  11103  absdifle  11104  retanclap  11732  tannegap  11738  lcmgcdeq  12085  isprm3  12120  prmdvdsexpb  12151  dvdsprmpweqnn  12337  mulgaddcomlem  13011  mulginvcom  13013  cnpf2  13746  blres  13973