Theorem syl3an2 1305

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

Syntax hints:   -> wi 4   /\ w3a 1002

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 1004

This theorem is referenced by:  syl3an2b  1308  syl3an2br  1311  syl3anl2  1320  nndi  6632  nnmass  6633  prarloclemarch2  7606  1idprl  7777  1idpru  7778  recexprlem1ssl  7820  recexprlem1ssu  7821  msqge0  8763  mulge0  8766  divsubdirap  8855  divdiv32ap  8867  peano2uz  9778  fzoshftral  10444  expdivap  10812  bcval5  10985  ccats1val1g  11170  redivap  11385  imdivap  11392  absdiflt  11603  absdifle  11604  retanclap  12233  tannegap  12239  lcmgcdeq  12605  isprm3  12640  prmdvdsexpb  12671  dvdsprmpweqnn  12859  mulgaddcomlem  13682  mulginvcom  13684  cnpf2  14881  blres  15108