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  6512  nnmass  6513  prarloclemarch2  7449  1idprl  7620  1idpru  7621  recexprlem1ssl  7663  recexprlem1ssu  7664  msqge0  8604  mulge0  8607  divsubdirap  8696  divdiv32ap  8708  peano2uz  9615  fzoshftral  10270  expdivap  10605  bcval5  10778  redivap  10918  imdivap  10925  absdiflt  11136  absdifle  11137  retanclap  11765  tannegap  11771  lcmgcdeq  12118  isprm3  12153  prmdvdsexpb  12184  dvdsprmpweqnn  12371  mulgaddcomlem  13102  mulginvcom  13104  cnpf2  14184  blres  14411