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  5866  fovcdmda  6021  smoiso  6306  tfrcl  6368  omv  6459  oeiv  6460  nndi  6490  nnmsucr  6492  f1oen2g  6758  f1dom2g  6759  undiffi  6927  prarloclemarch2  7421  distrnq0  7461  ltprordil  7591  1idprl  7592  1idpru  7593  ltpopr  7597  ltexprlemopu  7605  ltexprlemdisj  7608  ltexprlemfl  7611  ltexprlemfu  7613  ltexprlemru  7614  recexprlemdisj  7632  recexprlemss1l  7637  recexprlemss1u  7638  cnegexlem1  8135  msqge0  8576  mulge0  8579  divnegap  8666  divdiv32ap  8680  divneg2ap  8696  peano2uz  9586  lbzbi  9619  negqmod0  10334  modqmuladdnn0  10371  expnlbnd  10648  shftfvalg  10830  xrmaxaddlem  11271  retanclap  11733  tannegap  11739  demoivreALT  11784  gcd0id  11983  isprm3  12121  euclemma  12149  phiprmpw  12225  fermltl  12237  mndcl  12832  grpcl  12893  dfgrp2  12910  grprcan  12918  grpsubcl  12961  imasgrp2  12989  mhmid  12992  mhmmnd  12993  mulginvcom  13022  mulgnndir  13026  mulgnnass  13032  ablcom  13121  ablinvadd  13128  rngacl  13168  srgacl  13203  srgcom  13204  ringacl  13251  subrgacl  13391  subrgugrp  13399  lmodacl  13427  lmodmcl  13428  lmodvacl  13430  lmodvsubcl  13460  lmod4  13465  lmodvaddsub4  13467  lmodvpncan  13468  lmodvnpcan  13469  lmodsubeq0  13474  psmetcl  14014  xmetcl  14040  metcl  14041  meteq0  14048  metge0  14054  metsym  14059  blelrnps  14107  blelrn  14108  blssm  14109  blres  14122  mscl  14153  xmscl  14154  xmsge0  14155  xmseq0  14156  xmssym  14157  mopnin  14175  sincosq1sgn  14435  sincosq2sgn  14436  sincosq3sgn  14437  sincosq4sgn  14438  lgsneg1  14614