Theorem syl3an2 1283

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

Syntax hints:   -> wi 4   /\ w3a 980

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 982

This theorem is referenced by:  syl3an2b  1286  syl3an2br  1289  syl3anl2  1298  nndi  6544  nnmass  6545  prarloclemarch2  7486  1idprl  7657  1idpru  7658  recexprlem1ssl  7700  recexprlem1ssu  7701  msqge0  8643  mulge0  8646  divsubdirap  8735  divdiv32ap  8747  peano2uz  9657  fzoshftral  10314  expdivap  10682  bcval5  10855  redivap  11039  imdivap  11046  absdiflt  11257  absdifle  11258  retanclap  11887  tannegap  11893  lcmgcdeq  12251  isprm3  12286  prmdvdsexpb  12317  dvdsprmpweqnn  12505  mulgaddcomlem  13275  mulginvcom  13277  cnpf2  14443  blres  14670