Theorem syl3an2 1312

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

Syntax hints:   -> wi 4   /\ w3a 1009

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 1011

This theorem is referenced by:  syl3an2b  1315  syl3an2br  1318  syl3anl2  1327  nndi  6752  nnmass  6753  prarloclemarch2  7779  1idprl  7950  1idpru  7951  recexprlem1ssl  7993  recexprlem1ssu  7994  msqge0  8937  mulge0  8940  divsubdirap  9031  divdiv32ap  9043  peano2uz  9965  fzoshftral  10638  expdivap  11008  bcval5  11182  ccats1val1g  11388  redivap  11620  imdivap  11627  absdiflt  11839  absdifle  11840  retanclap  12470  tannegap  12476  lcmgcdeq  12842  isprm3  12877  prmdvdsexpb  12908  dvdsprmpweqnn  13096  mulgaddcomlem  13928  mulginvcom  13930  cnpf2  15234  blres  15461