Theorem syl3an2 1312

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

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  syl3an2b  1315  syl3an2br  1318  syl3anl2  1327  nndi  6759  nnmass  6760  prarloclemarch2  7787  1idprl  7958  1idpru  7959  recexprlem1ssl  8001  recexprlem1ssu  8002  msqge0  8947  mulge0  8950  divsubdirap  9041  divdiv32ap  9053  peano2uz  9993  fzoshftral  10668  expdivap  11042  bcval5  11217  ccats1val1g  11423  redivap  11655  imdivap  11662  absdiflt  11875  absdifle  11876  retanclap  12508  tannegap  12514  lcmgcdeq  12880  isprm3  12915  prmdvdsexpb  12947  dvdsprmpweqnn  13138  mulgaddcomlem  14001  mulginvcom  14003  cnpf2  15399  blres  15626