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  6697  nnmass  6698  prarloclemarch2  7699  1idprl  7870  1idpru  7871  recexprlem1ssl  7913  recexprlem1ssu  7914  msqge0  8855  mulge0  8858  divsubdirap  8947  divdiv32ap  8959  peano2uz  9878  fzoshftral  10547  expdivap  10915  bcval5  11088  ccats1val1g  11282  redivap  11514  imdivap  11521  absdiflt  11732  absdifle  11733  retanclap  12363  tannegap  12369  lcmgcdeq  12735  isprm3  12770  prmdvdsexpb  12801  dvdsprmpweqnn  12989  mulgaddcomlem  13812  mulginvcom  13814  cnpf2  15018  blres  15245