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  6487  nnmass  6488  prarloclemarch2  7418  1idprl  7589  1idpru  7590  recexprlem1ssl  7632  recexprlem1ssu  7633  msqge0  8573  mulge0  8576  divsubdirap  8665  divdiv32ap  8677  peano2uz  9583  fzoshftral  10238  expdivap  10571  bcval5  10743  redivap  10883  imdivap  10890  absdiflt  11101  absdifle  11102  retanclap  11730  tannegap  11736  lcmgcdeq  12083  isprm3  12118  prmdvdsexpb  12149  dvdsprmpweqnn  12335  mulgaddcomlem  13006  mulginvcom  13008  cnpf2  13710  blres  13937