Theorem syl3an1 1249

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 1167	. 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 962

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 964

This theorem is referenced by:  syl3an1b  1252  syl3an1br  1255  wepo  4281  f1ofveu  5762  fovrnda  5914  smoiso  6199  tfrcl  6261  omv  6351  oeiv  6352  nndi  6382  nnmsucr  6384  f1oen2g  6649  f1dom2g  6650  undiffi  6813  prarloclemarch2  7227  distrnq0  7267  ltprordil  7397  1idprl  7398  1idpru  7399  ltpopr  7403  ltexprlemopu  7411  ltexprlemdisj  7414  ltexprlemfl  7417  ltexprlemfu  7419  ltexprlemru  7420  recexprlemdisj  7438  recexprlemss1l  7443  recexprlemss1u  7444  cnegexlem1  7937  msqge0  8378  mulge0  8381  divnegap  8466  divdiv32ap  8480  divneg2ap  8496  peano2uz  9378  lbzbi  9408  negqmod0  10104  modqmuladdnn0  10141  expnlbnd  10416  shftfvalg  10590  xrmaxaddlem  11029  retanclap  11429  tannegap  11435  demoivreALT  11480  gcd0id  11667  isprm3  11799  euclemma  11824  phiprmpw  11898  psmetcl  12495  xmetcl  12521  metcl  12522  meteq0  12529  metge0  12535  metsym  12540  blelrnps  12588  blelrn  12589  blssm  12590  blres  12603  mscl  12634  xmscl  12635  xmsge0  12636  xmseq0  12637  xmssym  12638  mopnin  12656  sincosq1sgn  12907  sincosq2sgn  12908  sincosq3sgn  12909  sincosq4sgn  12910