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 )

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  syl3an2b  1315  syl3an2br  1318  syl3anl2  1327  nndi  6759  nnmass  6760  prarloclemarch2  7786  1idprl  7957  1idpru  7958  recexprlem1ssl  8000  recexprlem1ssu  8001  msqge0  8946  mulge0  8949  divsubdirap  9040  divdiv32ap  9052  peano2uz  9992  fzoshftral  10667  expdivap  11040  bcval5  11215  ccats1val1g  11421  redivap  11653  imdivap  11660  absdiflt  11873  absdifle  11874  retanclap  12505  tannegap  12511  lcmgcdeq  12877  isprm3  12912  prmdvdsexpb  12944  dvdsprmpweqnn  13135  mulgaddcomlem  13997  mulginvcom  13999  cnpf2  15357  blres  15584