Theorem syl3an2 1283

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

Syntax hints:   -> wi 4   /\ w3a 980

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 982

This theorem is referenced by:  syl3an2b  1286  syl3an2br  1289  syl3anl2  1298  nndi  6539  nnmass  6540  prarloclemarch2  7479  1idprl  7650  1idpru  7651  recexprlem1ssl  7693  recexprlem1ssu  7694  msqge0  8635  mulge0  8638  divsubdirap  8727  divdiv32ap  8739  peano2uz  9648  fzoshftral  10305  expdivap  10661  bcval5  10834  redivap  11018  imdivap  11025  absdiflt  11236  absdifle  11237  retanclap  11865  tannegap  11871  lcmgcdeq  12221  isprm3  12256  prmdvdsexpb  12287  dvdsprmpweqnn  12474  mulgaddcomlem  13215  mulginvcom  13217  cnpf2  14375  blres  14602