Theorem syl3an1 1271

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 1185	. 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 978

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

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  syl3an1b  1274  syl3an1br  1277  wepo  4361  f1ofveu  5865  fovcdmda  6020  smoiso  6305  tfrcl  6367  omv  6458  oeiv  6459  nndi  6489  nnmsucr  6491  f1oen2g  6757  f1dom2g  6758  undiffi  6926  prarloclemarch2  7420  distrnq0  7460  ltprordil  7590  1idprl  7591  1idpru  7592  ltpopr  7596  ltexprlemopu  7604  ltexprlemdisj  7607  ltexprlemfl  7610  ltexprlemfu  7612  ltexprlemru  7613  recexprlemdisj  7631  recexprlemss1l  7636  recexprlemss1u  7637  cnegexlem1  8134  msqge0  8575  mulge0  8578  divnegap  8665  divdiv32ap  8679  divneg2ap  8695  peano2uz  9585  lbzbi  9618  negqmod0  10333  modqmuladdnn0  10370  expnlbnd  10647  shftfvalg  10829  xrmaxaddlem  11270  retanclap  11732  tannegap  11738  demoivreALT  11783  gcd0id  11982  isprm3  12120  euclemma  12148  phiprmpw  12224  fermltl  12236  mndcl  12829  grpcl  12890  dfgrp2  12907  grprcan  12915  grpsubcl  12955  mhmid  12984  mhmmnd  12985  mulginvcom  13013  mulgnndir  13017  mulgnnass  13023  ablcom  13111  ablinvadd  13118  srgacl  13170  srgcom  13171  ringacl  13218  subrgacl  13358  subrgugrp  13366  lmodacl  13394  lmodmcl  13395  lmodvacl  13397  lmodvsubcl  13427  lmod4  13432  lmodvaddsub4  13434  lmodvpncan  13435  lmodvnpcan  13436  lmodsubeq0  13441  psmetcl  13865  xmetcl  13891  metcl  13892  meteq0  13899  metge0  13905  metsym  13910  blelrnps  13958  blelrn  13959  blssm  13960  blres  13973  mscl  14004  xmscl  14005  xmsge0  14006  xmseq0  14007  xmssym  14008  mopnin  14026  sincosq1sgn  14286  sincosq2sgn  14287  sincosq3sgn  14288  sincosq4sgn  14289  lgsneg1  14465