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  4406  f1ofveu  5932  fovcdmda  6090  smoiso  6388  tfrcl  6450  omv  6541  oeiv  6542  nndi  6572  nnmsucr  6574  f1oen2g  6846  f1dom2g  6847  undiffi  7022  prarloclemarch2  7532  distrnq0  7572  ltprordil  7702  1idprl  7703  1idpru  7704  ltpopr  7708  ltexprlemopu  7716  ltexprlemdisj  7719  ltexprlemfl  7722  ltexprlemfu  7724  ltexprlemru  7725  recexprlemdisj  7743  recexprlemss1l  7748  recexprlemss1u  7749  cnegexlem1  8247  msqge0  8689  mulge0  8692  divnegap  8779  divdiv32ap  8793  divneg2ap  8809  peano2uz  9704  lbzbi  9737  negqmod0  10476  modqmuladdnn0  10513  expnlbnd  10809  fun2dmnop  10993  shftfvalg  11129  xrmaxaddlem  11571  retanclap  12033  tannegap  12039  demoivreALT  12085  gcd0id  12300  isprm3  12440  euclemma  12468  phiprmpw  12544  fermltl  12556  sgrpcl  13241  mndcl  13255  imasmnd2  13284  grpcl  13340  dfgrp2  13359  grprcan  13369  grpsubcl  13412  imasgrp2  13446  mhmid  13451  mhmmnd  13452  mulginvcom  13483  mulgnndir  13487  mulgnnass  13493  qusgrp  13568  ghmmulg  13592  ghmrn  13593  ghmeqker  13607  ablcom  13639  ablinvadd  13646  ghmcmn  13663  rngacl  13704  rngpropd  13717  srgacl  13744  srgcom  13745  ringacl  13792  imasring  13826  subrngacl  13970  subrgacl  13994  subrgugrp  14002  lmodacl  14061  lmodmcl  14062  lmodvacl  14064  lmodvsubcl  14094  lmod4  14099  lmodvaddsub4  14101  lmodvpncan  14102  lmodvnpcan  14103  lmodsubeq0  14108  psmetcl  14798  xmetcl  14824  metcl  14825  meteq0  14832  metge0  14838  metsym  14843  blelrnps  14891  blelrn  14892  blssm  14893  blres  14906  mscl  14937  xmscl  14938  xmsge0  14939  xmseq0  14940  xmssym  14941  mopnin  14959  sincosq1sgn  15298  sincosq2sgn  15299  sincosq3sgn  15300  sincosq4sgn  15301  lgsneg1  15502