Theorem syl3an1 1250

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  1253  syl3an1br  1256  wepo  4289  f1ofveu  5770  fovrnda  5922  smoiso  6207  tfrcl  6269  omv  6359  oeiv  6360  nndi  6390  nnmsucr  6392  f1oen2g  6657  f1dom2g  6658  undiffi  6821  prarloclemarch2  7251  distrnq0  7291  ltprordil  7421  1idprl  7422  1idpru  7423  ltpopr  7427  ltexprlemopu  7435  ltexprlemdisj  7438  ltexprlemfl  7441  ltexprlemfu  7443  ltexprlemru  7444  recexprlemdisj  7462  recexprlemss1l  7467  recexprlemss1u  7468  cnegexlem1  7961  msqge0  8402  mulge0  8405  divnegap  8490  divdiv32ap  8504  divneg2ap  8520  peano2uz  9405  lbzbi  9435  negqmod0  10135  modqmuladdnn0  10172  expnlbnd  10447  shftfvalg  10622  xrmaxaddlem  11061  retanclap  11465  tannegap  11471  demoivreALT  11516  gcd0id  11703  isprm3  11835  euclemma  11860  phiprmpw  11934  psmetcl  12534  xmetcl  12560  metcl  12561  meteq0  12568  metge0  12574  metsym  12579  blelrnps  12627  blelrn  12628  blssm  12629  blres  12642  mscl  12673  xmscl  12674  xmsge0  12675  xmseq0  12676  xmssym  12677  mopnin  12695  sincosq1sgn  12955  sincosq2sgn  12956  sincosq3sgn  12957  sincosq4sgn  12958