Theorem syl3an2 1307

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

Syntax hints:   -> wi 4   /\ w3a 1004

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 1006

This theorem is referenced by:  syl3an2b  1310  syl3an2br  1313  syl3anl2  1322  nndi  6654  nnmass  6655  prarloclemarch2  7639  1idprl  7810  1idpru  7811  recexprlem1ssl  7853  recexprlem1ssu  7854  msqge0  8796  mulge0  8799  divsubdirap  8888  divdiv32ap  8900  peano2uz  9817  fzoshftral  10484  expdivap  10852  bcval5  11025  ccats1val1g  11216  redivap  11435  imdivap  11442  absdiflt  11653  absdifle  11654  retanclap  12284  tannegap  12290  lcmgcdeq  12656  isprm3  12691  prmdvdsexpb  12722  dvdsprmpweqnn  12910  mulgaddcomlem  13733  mulginvcom  13735  cnpf2  14933  blres  15160