Theorem syl3an2 1284

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

Syntax hints:   -> wi 4   /\ w3a 981

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 983

This theorem is referenced by:  syl3an2b  1287  syl3an2br  1290  syl3anl2  1299  nndi  6595  nnmass  6596  prarloclemarch2  7567  1idprl  7738  1idpru  7739  recexprlem1ssl  7781  recexprlem1ssu  7782  msqge0  8724  mulge0  8727  divsubdirap  8816  divdiv32ap  8828  peano2uz  9739  fzoshftral  10404  expdivap  10772  bcval5  10945  ccats1val1g  11129  redivap  11300  imdivap  11307  absdiflt  11518  absdifle  11519  retanclap  12148  tannegap  12154  lcmgcdeq  12520  isprm3  12555  prmdvdsexpb  12586  dvdsprmpweqnn  12774  mulgaddcomlem  13596  mulginvcom  13598  cnpf2  14794  blres  15021