Theorem syl3an1 1283

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 1188	. 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 981

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 983

This theorem is referenced by:  syl3an1b  1286  syl3an1br  1289  wepo  4424  f1ofveu  5955  fovcdmda  6113  smoiso  6411  tfrcl  6473  omv  6564  oeiv  6565  nndi  6595  nnmsucr  6597  f1oen2g  6869  f1dom2g  6870  undiffi  7048  prarloclemarch2  7567  distrnq0  7607  ltprordil  7737  1idprl  7738  1idpru  7739  ltpopr  7743  ltexprlemopu  7751  ltexprlemdisj  7754  ltexprlemfl  7757  ltexprlemfu  7759  ltexprlemru  7760  recexprlemdisj  7778  recexprlemss1l  7783  recexprlemss1u  7784  cnegexlem1  8282  msqge0  8724  mulge0  8727  divnegap  8814  divdiv32ap  8828  divneg2ap  8844  peano2uz  9739  lbzbi  9772  negqmod0  10513  modqmuladdnn0  10550  expnlbnd  10846  fun2dmnop  11030  shftfvalg  11244  xrmaxaddlem  11686  retanclap  12148  tannegap  12154  demoivreALT  12200  gcd0id  12415  isprm3  12555  euclemma  12583  phiprmpw  12659  fermltl  12671  sgrpcl  13356  mndcl  13370  imasmnd2  13399  grpcl  13455  dfgrp2  13474  grprcan  13484  grpsubcl  13527  imasgrp2  13561  mhmid  13566  mhmmnd  13567  mulginvcom  13598  mulgnndir  13602  mulgnnass  13608  qusgrp  13683  ghmmulg  13707  ghmrn  13708  ghmeqker  13722  ablcom  13754  ablinvadd  13761  ghmcmn  13778  rngacl  13819  rngpropd  13832  srgacl  13859  srgcom  13860  ringacl  13907  imasring  13941  subrngacl  14085  subrgacl  14109  subrgugrp  14117  lmodacl  14176  lmodmcl  14177  lmodvacl  14179  lmodvsubcl  14209  lmod4  14214  lmodvaddsub4  14216  lmodvpncan  14217  lmodvnpcan  14218  lmodsubeq0  14223  psmetcl  14913  xmetcl  14939  metcl  14940  meteq0  14947  metge0  14953  metsym  14958  blelrnps  15006  blelrn  15007  blssm  15008  blres  15021  mscl  15052  xmscl  15053  xmsge0  15054  xmseq0  15055  xmssym  15056  mopnin  15074  sincosq1sgn  15413  sincosq2sgn  15414  sincosq3sgn  15415  sincosq4sgn  15416  lgsneg1  15617