Theorem syl3an1 1261

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 1175	. 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 968

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

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  syl3an1b  1264  syl3an1br  1267  wepo  4337  f1ofveu  5830  fovrnda  5985  smoiso  6270  tfrcl  6332  omv  6423  oeiv  6424  nndi  6454  nnmsucr  6456  f1oen2g  6721  f1dom2g  6722  undiffi  6890  prarloclemarch2  7360  distrnq0  7400  ltprordil  7530  1idprl  7531  1idpru  7532  ltpopr  7536  ltexprlemopu  7544  ltexprlemdisj  7547  ltexprlemfl  7550  ltexprlemfu  7552  ltexprlemru  7553  recexprlemdisj  7571  recexprlemss1l  7576  recexprlemss1u  7577  cnegexlem1  8073  msqge0  8514  mulge0  8517  divnegap  8602  divdiv32ap  8616  divneg2ap  8632  peano2uz  9521  lbzbi  9554  negqmod0  10266  modqmuladdnn0  10303  expnlbnd  10579  shftfvalg  10760  xrmaxaddlem  11201  retanclap  11663  tannegap  11669  demoivreALT  11714  gcd0id  11912  isprm3  12050  euclemma  12078  phiprmpw  12154  fermltl  12166  psmetcl  12966  xmetcl  12992  metcl  12993  meteq0  13000  metge0  13006  metsym  13011  blelrnps  13059  blelrn  13060  blssm  13061  blres  13074  mscl  13105  xmscl  13106  xmsge0  13107  xmseq0  13108  xmssym  13109  mopnin  13127  sincosq1sgn  13387  sincosq2sgn  13388  sincosq3sgn  13389  sincosq4sgn  13390  lgsneg1  13566