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  4387  tz7.5  4413  fovrnda  5991  f1ofveu  6339  smoiso  6379  odi  6577  nndi  6621  nnmsucr  6623  f1oen2g  6878  f1dom2g  6879  domssex2  7021  ordunifi  7107  wemappo  7264  wemapso  7266  wemapso2  7267  ackbij1lem16  7861  divneg  9455  divdiv32  9468  divneg2  9484  ltdiv2  9641  fimaxre  9701  suprzcl  10091  peano2uz  10272  infmssuzle  10300  lbzbi  10306  zbtwnre  10314  irrmul  10341  supxrunb1  10638  expnlbnd  11231  retancl  12422  tanneg  12428  demoivreALT  12481  dvdscmulr  12557  dvdsmulcr  12558  gcd0id  12702  euclemma  12787  phiprmpw  12844  fermltl  12852  vdwapun  13021  vdwapid1  13022  pospo  14107  latasymb  14160  latjle12  14168  latlem12  14184  imasmnd2  14409  grpcl  14495  grprcan  14515  grpsubcl  14546  imasgrp2  14610  divsgrp  14672  ghmmulg  14695  ghmrn  14696  ghmeqker  14709  ablcom  15106  ablinvadd  15111  mulgmhm  15127  mulgghm  15128  odadd1  15140  odadd2  15141  rngcl  15354  crngcom  15355  rngacl  15368  imasrng  15402  irredlmul  15490  rhmmul  15505  drngmcl  15525  isdrngd  15537  subrgacl  15556  subrgugrp  15564  srngadd  15622  srngmul  15623  lmodacl  15638  lmodmcl  15639  lmodvacl  15641  lmodvsubcl  15670  lmod4  15675  lmodvaddsub4  15677  lmodvpncan  15678  lmodvnpcan  15679  lmodsubeq0  15684  islbs2  15907  islbs3  15908  lbsext  15916  rspssp  15978  mplbas2  16212  coe1add  16341  coe1subfv  16343  coe1mul2  16346  zlmlmod  16477  ipdir  16543  ip2eq  16557  ocvin  16574  filin  17549  filfinnfr  17572  filuni  17580  ufprim  17604  uffinfix  17622  hausflf  17692  uffcfflf  17734  tmdmulg  17775  tsmsxplem1  17835  xmetcl  17896  metcl  17897  meteq0  17904  metge0  17910  metsym  17914  metgt0  17923  blelrn  17967  blssm  17968  blres  17977  mscl  18007  xmscl  18008  xmsge0  18009  xmseq0  18010  xmssym  18011  mopnin  18043  nmf2  18115  ngpdsr  18126  ngpds2  18127  ngpds2r  18128  ngpds3  18129  ngpds3r  18130  nmge0  18138  nmeq0  18139  nm2dif  18146  nmmul  18175  nlmmul0or  18194  nmods  18253  clmsub  18578  clmacl  18581  clmmcl  18582  clmsubcl  18583  cphnmvs  18626  cphipcl  18627  cphipcj  18635  cphorthcom  18636  fmcfil  18698  mbfi1fseqlem3  19072  mbfi1fseqlem4  19073  mbfi1fseqlem5  19074  evlsrhm  19405  deg1ldgdomn  19480  drnguc1p  19556  quotval  19672  sincosq1sgn  19866  sincosq2sgn  19867  sincosq3sgn  19868  sincosq4sgn  19869  lgsneg1  20559  dchrisumlem3  20640  grpocl  20867  grpodivcl  20914  ablomuldiv  20956  ablodivdiv4  20958  ablonnncan  20960  ablonnncan1  20962  gxdi  20963  rngocl  21049  rngogcl  21058  rngocom  21059  rngoa4  21062  vccl  21106  vcgcl  21115  vccom  21116  vca4  21119  nvgcl  21176  nvcom  21177  nvadd4  21183  nvscl  21184  nvmval  21200  nvmcl  21205  nmcvcn  21268  nmlnoubi  21374  isblo3i  21379  blometi  21381  dipsubdir  21426  hlpar2  21475  hlpar  21476  hlcom  21479  hlipcj  21490  hlipgt0  21493  his52  21666  shintcli  21908  chlub  22088  homulass  22382  adjadj  22516  nmophmi  22611  kbass6  22701  atcvatlem  22965  mdsymlem3  22985  mdsymlem5  22987  rexdiv  23109  probdif  23623  climuzcnv  24004  ax5seglem2  24557  abloinvop  25353  sum2vv  25462  prodvs  25468  prvs  25478  flfneih  25560  limfn3  25567  flfnein  25621  cmppfcd  25770  domcmpc  25771  codcmpc  25772  eqidob  25795  ssbnd  26512  heibor1  26534  exidcl  26566  rngosub  26579  rngonegmn1l  26580  rngonegmn1r  26581  ispridlc  26695  pwssplit3  27190  frlmsplit2  27243  rngvcl  27453  sinhpcosh  28210  reseccl  28223  recsccl  28224  recotcl  28225  onetansqsecsq  28231  eelT00  28480  eelTTT  28481  eelT11  28483  eelT12  28486  eelTT1  28488  eelT01  28489  lshpcmp  29178  op0le  29376  ople1  29381  opltcon3b  29394  oldmm1  29407  olj01  29415  latm32  29421  omllaw4  29436  omllaw5N  29437  cmtcomlemN  29438  cmt2N  29440  cmtbr2N  29443  cmtbr3N  29444  cmtbr4N  29445  atl0le  29494  glbconxN  29567  hlexch1  29571  hlexch2  29572  hlexchb1  29573  hlexchb2  29574  hlexch3  29580  hlexch4N  29581  hlatexchb1  29582  hlatexchb2  29583  hlatexch1  29584  hlatexch2  29585  hlatle  29587  hlateq  29588  hlrelat1  29589  hlrelat2  29592  cvr1  29599  cvrval5  29604  cvrp  29605  atcvr1  29606  atcvr2  29607  cvrexchlem  29608  cvrexch  29609  dalem54  29915  pmaple  29950  pmap11  29951  paddass  30027  pmapj2N  30118  pmapocjN  30119  trlval2  30352
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