Theorem syl3an2 1272

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

Syntax hints:   -> wi 4   /\ w3a 978

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 980

This theorem is referenced by:  syl3an2b  1275  syl3an2br  1278  syl3anl2  1287  nndi  6477  nnmass  6478  prarloclemarch2  7393  1idprl  7564  1idpru  7565  recexprlem1ssl  7607  recexprlem1ssu  7608  msqge0  8547  mulge0  8550  divsubdirap  8637  divdiv32ap  8649  peano2uz  9554  fzoshftral  10206  expdivap  10539  bcval5  10709  redivap  10849  imdivap  10856  absdiflt  11067  absdifle  11068  retanclap  11696  tannegap  11702  lcmgcdeq  12048  isprm3  12083  prmdvdsexpb  12114  dvdsprmpweqnn  12300  mulgaddcomlem  12864  mulginvcom  12866  cnpf2  13258  blres  13485