Theorem syl3an2 1250

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

Syntax hints:   -> wi 4   /\ w3a 962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  syl3an2b  1253  syl3an2br  1256  syl3anl2  1265  nndi  6375  nnmass  6376  prarloclemarch2  7220  1idprl  7391  1idpru  7392  recexprlem1ssl  7434  recexprlem1ssu  7435  msqge0  8371  mulge0  8374  divsubdirap  8461  divdiv32ap  8473  peano2uz  9371  fzoshftral  10008  expdivap  10337  bcval5  10502  redivap  10639  imdivap  10646  absdiflt  10857  absdifle  10858  retanclap  11418  tannegap  11424  lcmgcdeq  11753  isprm3  11788  prmdvdsexpb  11816  cnpf2  12365  blres  12592