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  6657  nnmass  6658  prarloclemarch2  7642  1idprl  7813  1idpru  7814  recexprlem1ssl  7856  recexprlem1ssu  7857  msqge0  8799  mulge0  8802  divsubdirap  8891  divdiv32ap  8903  peano2uz  9820  fzoshftral  10488  expdivap  10856  bcval5  11029  ccats1val1g  11223  redivap  11455  imdivap  11462  absdiflt  11673  absdifle  11674  retanclap  12304  tannegap  12310  lcmgcdeq  12676  isprm3  12711  prmdvdsexpb  12742  dvdsprmpweqnn  12930  mulgaddcomlem  13753  mulginvcom  13755  cnpf2  14958  blres  15185