Theorem syl3an2 1308

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

Syntax hints:   -> wi 4   /\ w3a 1005

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 1007

This theorem is referenced by:  syl3an2b  1311  syl3an2br  1314  syl3anl2  1323  nndi  6721  nnmass  6722  prarloclemarch2  7736  1idprl  7907  1idpru  7908  recexprlem1ssl  7950  recexprlem1ssu  7951  msqge0  8892  mulge0  8895  divsubdirap  8984  divdiv32ap  8996  peano2uz  9918  fzoshftral  10588  expdivap  10956  bcval5  11129  ccats1val1g  11331  redivap  11563  imdivap  11570  absdiflt  11781  absdifle  11782  retanclap  12412  tannegap  12418  lcmgcdeq  12784  isprm3  12819  prmdvdsexpb  12850  dvdsprmpweqnn  13038  mulgaddcomlem  13879  mulginvcom  13881  cnpf2  15089  blres  15316