Theorem syl3an2 1262

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

Syntax hints:   -> wi 4   /\ w3a 968

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 970

This theorem is referenced by:  syl3an2b  1265  syl3an2br  1268  syl3anl2  1277  nndi  6454  nnmass  6455  prarloclemarch2  7360  1idprl  7531  1idpru  7532  recexprlem1ssl  7574  recexprlem1ssu  7575  msqge0  8514  mulge0  8517  divsubdirap  8604  divdiv32ap  8616  peano2uz  9521  fzoshftral  10173  expdivap  10506  bcval5  10676  redivap  10816  imdivap  10823  absdiflt  11034  absdifle  11035  retanclap  11663  tannegap  11669  lcmgcdeq  12015  isprm3  12050  prmdvdsexpb  12081  dvdsprmpweqnn  12267  cnpf2  12847  blres  13074