Theorem syl3an1 1202

Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)

Hypotheses

Ref	Expression
syl3an1.1	|- ( ph -> ps )
syl3an1.2	|- ( ( ps /\ ch /\ th ) -> ta )

Assertion

Ref	Expression
syl3an1	|- ( ( ph /\ ch /\ th ) -> ta )

Proof of Theorem syl3an1

Step	Hyp	Ref	Expression
1		syl3an1.1	. . 3 |- ( ph -> ps )
2	1	3anim1i 1124	. 2 |- ( ( ph /\ ch /\ th ) -> ( ps /\ ch /\ th ) )
3		syl3an1.2	. 2 |- ( ( ps /\ ch /\ th ) -> ta )
4	2, 3	syl 14	1 |- ( ( ph /\ ch /\ th ) -> ta )

Syntax hints:   -> wi 4   /\ w3a 919

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

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  syl3an1b  1205  syl3an1br  1208  wepo  4114  f1ofveu  5520  fovrnda  5664  smoiso  5940  omv  6058  oeiv  6059  nndi  6088  nnmsucr  6090  f1oen2g  6258  f1dom2g  6259  prarloclemarch2  6609  distrnq0  6649  ltprordil  6779  1idprl  6780  1idpru  6781  ltpopr  6785  ltexprlemopu  6793  ltexprlemdisj  6796  ltexprlemfl  6799  ltexprlemfu  6801  ltexprlemru  6802  recexprlemdisj  6820  recexprlemss1l  6825  recexprlemss1u  6826  cnegexlem1  7283  msqge0  7716  mulge0  7719  divnegap  7794  divdiv32ap  7808  divneg2ap  7824  peano2uz  8671  lbzbi  8701  negqmod0  9333  modqmuladdnn0  9370  expnlbnd  9597  shftfvalg  9706  gcd0id  10370  isprm3  10500  euclemma  10525