Theorem syl3an1 1282

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 1187	. 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 980

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 982

This theorem is referenced by:  syl3an1b  1285  syl3an1br  1288  wepo  4391  f1ofveu  5907  fovcdmda  6064  smoiso  6357  tfrcl  6419  omv  6510  oeiv  6511  nndi  6541  nnmsucr  6543  f1oen2g  6811  f1dom2g  6812  undiffi  6983  prarloclemarch2  7481  distrnq0  7521  ltprordil  7651  1idprl  7652  1idpru  7653  ltpopr  7657  ltexprlemopu  7665  ltexprlemdisj  7668  ltexprlemfl  7671  ltexprlemfu  7673  ltexprlemru  7674  recexprlemdisj  7692  recexprlemss1l  7697  recexprlemss1u  7698  cnegexlem1  8196  msqge0  8637  mulge0  8640  divnegap  8727  divdiv32ap  8741  divneg2ap  8757  peano2uz  9651  lbzbi  9684  negqmod0  10405  modqmuladdnn0  10442  expnlbnd  10738  shftfvalg  10965  xrmaxaddlem  11406  retanclap  11868  tannegap  11874  demoivreALT  11920  gcd0id  12119  isprm3  12259  euclemma  12287  phiprmpw  12363  fermltl  12375  sgrpcl  12995  mndcl  13007  grpcl  13083  dfgrp2  13102  grprcan  13112  grpsubcl  13155  imasgrp2  13183  mhmid  13188  mhmmnd  13189  mulginvcom  13220  mulgnndir  13224  mulgnnass  13230  qusgrp  13305  ghmmulg  13329  ghmrn  13330  ghmeqker  13344  ablcom  13376  ablinvadd  13383  ghmcmn  13400  rngacl  13441  rngpropd  13454  srgacl  13481  srgcom  13482  ringacl  13529  imasring  13563  subrngacl  13707  subrgacl  13731  subrgugrp  13739  lmodacl  13798  lmodmcl  13799  lmodvacl  13801  lmodvsubcl  13831  lmod4  13836  lmodvaddsub4  13838  lmodvpncan  13839  lmodvnpcan  13840  lmodsubeq0  13845  psmetcl  14505  xmetcl  14531  metcl  14532  meteq0  14539  metge0  14545  metsym  14550  blelrnps  14598  blelrn  14599  blssm  14600  blres  14613  mscl  14644  xmscl  14645  xmsge0  14646  xmseq0  14647  xmssym  14648  mopnin  14666  sincosq1sgn  15002  sincosq2sgn  15003  sincosq3sgn  15004  sincosq4sgn  15005  lgsneg1  15182