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  6541  nnmass  6542  prarloclemarch2  7481  1idprl  7652  1idpru  7653  recexprlem1ssl  7695  recexprlem1ssu  7696  msqge0  8637  mulge0  8640  divsubdirap  8729  divdiv32ap  8741  peano2uz  9651  fzoshftral  10308  expdivap  10664  bcval5  10837  redivap  11021  imdivap  11028  absdiflt  11239  absdifle  11240  retanclap  11868  tannegap  11874  lcmgcdeq  12224  isprm3  12259  prmdvdsexpb  12290  dvdsprmpweqnn  12477  mulgaddcomlem  13218  mulginvcom  13220  cnpf2  14386  blres  14613