Theorem syl3an1 1304

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 1209	. 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 1002

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 1004

This theorem is referenced by:  syl3an1b  1307  syl3an1br  1310  wepo  4450  f1ofveu  5995  fovcdmda  6155  smoiso  6454  tfrcl  6516  omv  6609  oeiv  6610  nndi  6640  nnmsucr  6642  f1oen2g  6914  f1dom2g  6915  undiffi  7098  prarloclemarch2  7617  distrnq0  7657  ltprordil  7787  1idprl  7788  1idpru  7789  ltpopr  7793  ltexprlemopu  7801  ltexprlemdisj  7804  ltexprlemfl  7807  ltexprlemfu  7809  ltexprlemru  7810  recexprlemdisj  7828  recexprlemss1l  7833  recexprlemss1u  7834  cnegexlem1  8332  msqge0  8774  mulge0  8777  divnegap  8864  divdiv32ap  8878  divneg2ap  8894  peano2uz  9790  lbzbi  9823  negqmod0  10565  modqmuladdnn0  10602  expnlbnd  10898  fun2dmnop  11083  shftfvalg  11345  xrmaxaddlem  11787  retanclap  12249  tannegap  12255  demoivreALT  12301  gcd0id  12516  isprm3  12656  euclemma  12684  phiprmpw  12760  fermltl  12772  sgrpcl  13458  mndcl  13472  imasmnd2  13501  grpcl  13557  dfgrp2  13576  grprcan  13586  grpsubcl  13629  imasgrp2  13663  mhmid  13668  mhmmnd  13669  mulginvcom  13700  mulgnndir  13704  mulgnnass  13710  qusgrp  13785  ghmmulg  13809  ghmrn  13810  ghmeqker  13824  ablcom  13856  ablinvadd  13863  ghmcmn  13880  rngacl  13921  rngpropd  13934  srgacl  13961  srgcom  13962  ringacl  14009  imasring  14043  subrngacl  14188  subrgacl  14212  subrgugrp  14220  lmodacl  14279  lmodmcl  14280  lmodvacl  14282  lmodvsubcl  14312  lmod4  14317  lmodvaddsub4  14319  lmodvpncan  14320  lmodvnpcan  14321  lmodsubeq0  14326  psmetcl  15016  xmetcl  15042  metcl  15043  meteq0  15050  metge0  15056  metsym  15061  blelrnps  15109  blelrn  15110  blssm  15111  blres  15124  mscl  15155  xmscl  15156  xmsge0  15157  xmseq0  15158  xmssym  15159  mopnin  15177  sincosq1sgn  15516  sincosq2sgn  15517  sincosq3sgn  15518  sincosq4sgn  15519  lgsneg1  15720  usgredg2vtx  16031  uspgredg2vtxeu  16032  usgredg2vtxeu  16033