Theorem syl3an2 1267

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

Syntax hints:   -> wi 4   /\ w3a 973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  syl3an2b  1270  syl3an2br  1273  syl3anl2  1282  nndi  6465  nnmass  6466  prarloclemarch2  7381  1idprl  7552  1idpru  7553  recexprlem1ssl  7595  recexprlem1ssu  7596  msqge0  8535  mulge0  8538  divsubdirap  8625  divdiv32ap  8637  peano2uz  9542  fzoshftral  10194  expdivap  10527  bcval5  10697  redivap  10838  imdivap  10845  absdiflt  11056  absdifle  11057  retanclap  11685  tannegap  11691  lcmgcdeq  12037  isprm3  12072  prmdvdsexpb  12103  dvdsprmpweqnn  12289  cnpf2  13001  blres  13228