Theorem syl3an1 1253

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 1168	. 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 963

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 965

This theorem is referenced by:  syl3an1b  1256  syl3an1br  1259  wepo  4322  f1ofveu  5815  fovrnda  5967  smoiso  6252  tfrcl  6314  omv  6405  oeiv  6406  nndi  6436  nnmsucr  6438  f1oen2g  6703  f1dom2g  6704  undiffi  6872  prarloclemarch2  7342  distrnq0  7382  ltprordil  7512  1idprl  7513  1idpru  7514  ltpopr  7518  ltexprlemopu  7526  ltexprlemdisj  7529  ltexprlemfl  7532  ltexprlemfu  7534  ltexprlemru  7535  recexprlemdisj  7553  recexprlemss1l  7558  recexprlemss1u  7559  cnegexlem1  8055  msqge0  8496  mulge0  8499  divnegap  8584  divdiv32ap  8598  divneg2ap  8614  peano2uz  9500  lbzbi  9532  negqmod0  10240  modqmuladdnn0  10277  expnlbnd  10552  shftfvalg  10730  xrmaxaddlem  11169  retanclap  11631  tannegap  11637  demoivreALT  11682  gcd0id  11879  isprm3  12011  euclemma  12037  phiprmpw  12113  fermltl  12125  psmetcl  12822  xmetcl  12848  metcl  12849  meteq0  12856  metge0  12862  metsym  12867  blelrnps  12915  blelrn  12916  blssm  12917  blres  12930  mscl  12961  xmscl  12962  xmsge0  12963  xmseq0  12964  xmssym  12965  mopnin  12983  sincosq1sgn  13243  sincosq2sgn  13244  sincosq3sgn  13245  sincosq4sgn  13246