MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl3an1 Unicode version

Theorem syl3an1 1215
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
StepHypRef Expression
1 syl3an1.1 . . 3  |-  ( ph  ->  ps )
213anim1i 1138 . 2  |-  ( (
ph  /\  ch  /\  th )  ->  ( ps  /\  ch  /\  th ) )
3 syl3an1.2 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ta )
42, 3syl 15 1  |-  ( (
ph  /\  ch  /\  th )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  syl3an1b  1218  syl3an1br  1221  wefrc  4403  tz7.5  4429  fovrnda  6007  f1ofveu  6355  smoiso  6395  odi  6593  nndi  6637  nnmsucr  6639  f1oen2g  6894  f1dom2g  6895  domssex2  7037  ordunifi  7123  wemappo  7280  wemapso  7282  wemapso2  7283  ackbij1lem16  7877  divneg  9471  divdiv32  9484  divneg2  9500  ltdiv2  9657  fimaxre  9717  suprzcl  10107  peano2uz  10288  infmssuzle  10316  lbzbi  10322  zbtwnre  10330  irrmul  10357  supxrunb1  10654  expnlbnd  11247  retancl  12438  tanneg  12444  demoivreALT  12497  dvdscmulr  12573  dvdsmulcr  12574  gcd0id  12718  euclemma  12803  phiprmpw  12860  fermltl  12868  vdwapun  13037  vdwapid1  13038  pospo  14123  latasymb  14176  latjle12  14184  latlem12  14200  imasmnd2  14425  grpcl  14511  grprcan  14531  grpsubcl  14562  imasgrp2  14626  divsgrp  14688  ghmmulg  14711  ghmrn  14712  ghmeqker  14725  ablcom  15122  ablinvadd  15127  mulgmhm  15143  mulgghm  15144  odadd1  15156  odadd2  15157  rngcl  15370  crngcom  15371  rngacl  15384  imasrng  15418  irredlmul  15506  rhmmul  15521  drngmcl  15541  isdrngd  15553  subrgacl  15572  subrgugrp  15580  srngadd  15638  srngmul  15639  lmodacl  15654  lmodmcl  15655  lmodvacl  15657  lmodvsubcl  15686  lmod4  15691  lmodvaddsub4  15693  lmodvpncan  15694  lmodvnpcan  15695  lmodsubeq0  15700  islbs2  15923  islbs3  15924  lbsext  15932  rspssp  15994  mplbas2  16228  coe1add  16357  coe1subfv  16359  coe1mul2  16362  zlmlmod  16493  ipdir  16559  ip2eq  16573  ocvin  16590  filin  17565  filfinnfr  17588  filuni  17596  ufprim  17620  uffinfix  17638  hausflf  17708  uffcfflf  17750  tmdmulg  17791  tsmsxplem1  17851  xmetcl  17912  metcl  17913  meteq0  17920  metge0  17926  metsym  17930  metgt0  17939  blelrn  17983  blssm  17984  blres  17993  mscl  18023  xmscl  18024  xmsge0  18025  xmseq0  18026  xmssym  18027  mopnin  18059  nmf2  18131  ngpdsr  18142  ngpds2  18143  ngpds2r  18144  ngpds3  18145  ngpds3r  18146  nmge0  18154  nmeq0  18155  nm2dif  18162  nmmul  18191  nlmmul0or  18210  nmods  18269  clmsub  18594  clmacl  18597  clmmcl  18598  clmsubcl  18599  cphnmvs  18642  cphipcl  18643  cphipcj  18651  cphorthcom  18652  fmcfil  18714  mbfi1fseqlem3  19088  mbfi1fseqlem4  19089  mbfi1fseqlem5  19090  evlsrhm  19421  deg1ldgdomn  19496  drnguc1p  19572  quotval  19688  sincosq1sgn  19882  sincosq2sgn  19883  sincosq3sgn  19884  sincosq4sgn  19885  lgsneg1  20575  dchrisumlem3  20656  grpocl  20883  grpodivcl  20930  ablomuldiv  20972  ablodivdiv4  20974  ablonnncan  20976  ablonnncan1  20978  gxdi  20979  rngocl  21065  rngogcl  21074  rngocom  21075  rngoa4  21078  vccl  21122  vcgcl  21131  vccom  21132  vca4  21135  nvgcl  21192  nvcom  21193  nvadd4  21199  nvscl  21200  nvmval  21216  nvmcl  21221  nmcvcn  21284  nmlnoubi  21390  isblo3i  21395  blometi  21397  dipsubdir  21442  hlpar2  21491  hlpar  21492  hlcom  21495  hlipcj  21506  hlipgt0  21509  his52  21682  shintcli  21924  chlub  22104  homulass  22398  adjadj  22532  nmophmi  22627  kbass6  22717  atcvatlem  22981  mdsymlem3  23001  mdsymlem5  23003  rexdiv  23125  probdif  23638  climuzcnv  24019  ax5seglem2  24629  abloinvop  25456  sum2vv  25565  prodvs  25571  prvs  25581  flfneih  25663  limfn3  25670  flfnein  25724  cmppfcd  25873  domcmpc  25874  codcmpc  25875  eqidob  25898  ssbnd  26615  heibor1  26637  exidcl  26669  rngosub  26682  rngonegmn1l  26683  rngonegmn1r  26684  ispridlc  26798  pwssplit3  27293  frlmsplit2  27346  rngvcl  27556  wlkdvspthlem  28365  sinhpcosh  28464  reseccl  28477  recsccl  28478  recotcl  28479  onetansqsecsq  28485  eelT00  28785  eelTTT  28786  eelT11  28788  eelT12  28792  eelTT1  28794  eelT01  28795  lshpcmp  29800  op0le  29998  ople1  30003  opltcon3b  30016  oldmm1  30029  olj01  30037  latm32  30043  omllaw4  30058  omllaw5N  30059  cmtcomlemN  30060  cmt2N  30062  cmtbr2N  30065  cmtbr3N  30066  cmtbr4N  30067  atl0le  30116  glbconxN  30189  hlexch1  30193  hlexch2  30194  hlexchb1  30195  hlexchb2  30196  hlexch3  30202  hlexch4N  30203  hlatexchb1  30204  hlatexchb2  30205  hlatexch1  30206  hlatexch2  30207  hlatle  30209  hlateq  30210  hlrelat1  30211  hlrelat2  30214  cvr1  30221  cvrval5  30226  cvrp  30227  atcvr1  30228  atcvr2  30229  cvrexchlem  30230  cvrexch  30231  dalem54  30537  pmaple  30572  pmap11  30573  paddass  30649  pmapj2N  30740  pmapocjN  30741  trlval2  30974
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator