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  6572  nnmass  6573  prarloclemarch2  7532  1idprl  7703  1idpru  7704  recexprlem1ssl  7746  recexprlem1ssu  7747  msqge0  8689  mulge0  8692  divsubdirap  8781  divdiv32ap  8793  peano2uz  9704  fzoshftral  10367  expdivap  10735  bcval5  10908  ccats1val1g  11091  redivap  11185  imdivap  11192  absdiflt  11403  absdifle  11404  retanclap  12033  tannegap  12039  lcmgcdeq  12405  isprm3  12440  prmdvdsexpb  12471  dvdsprmpweqnn  12659  mulgaddcomlem  13481  mulginvcom  13483  cnpf2  14679  blres  14906