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

Theorem syl3an2 1262
Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)
Hypotheses
Ref Expression
syl3an2.1
syl3an2.2
Assertion
Ref Expression
syl3an2

Proof of Theorem syl3an2
StepHypRef Expression
1 syl3an2.1 . . 3
2 syl3an2.2 . . . 4
323exp 1195 . . 3
41, 3syl5 32 . 2
543imp 1190 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\w3a 973
This theorem is referenced by:  syl3an2b  1265  syl3an2br  1268  syl3anl2  1277  odi  7247  omass  7248  nndi  7291  nnmass  7292  omabslem  7314  winainf  9093  divsubdir  10265  divdiv32  10277  ltdiv2  10455  peano2uz  11163  irrmul  11236  supxrunb1  11540  fzoshftral  11923  ltdifltdiv  11966  axdc4uzlem  12092  expdiv  12216  bcval5  12396  ccats1val1  12630  rediv  12964  imdiv  12971  absdiflt  13150  absdifle  13151  iseraltlem3  13506  retancl  13877  tanneg  13883  prmdvdsexpb  14256  pmtrfb  16490  lspssp  17634  mdetunilem7  19120  m2detleiblem3  19131  m2detleiblem4  19132  pmatcollpw  19282  pmatcollpwscmat  19292  chpmatply1  19333  chfacfscmulgsum  19361  chfacfpmmulcl  19362  chfacfpmmul0  19363  chfacfpmmulgsum  19365  chfacfpmmulgsum2  19366  cayhamlem1  19367  cpmadurid  19368  cpmadugsumlemC  19376  cpmadugsumlemF  19377  cpmadugsumfi  19378  cpmidgsum2  19380  islp2  19646  fmfg  20450  fmufil  20460  flffbas  20496  lmflf  20506  uffcfflf  20540  blres  20934  caucfil  21722  cmetcusp1OLD  21791  cmetcusp1  21792  deg1mul3  22516  quotval  22688  cusgra3vnbpr  24465  gxid  25275  nvsge0  25566  hvsubass  25961  hvsubdistr2  25967  hvsubcan  25991  his2sub  26009  chlub  26427  spanunsni  26497  homco1  26720  homulass  26721  cnlnadjlem2  26987  adjmul  27011  chirredlem2  27310  atmd2  27319  mdsymlem5  27326  climuzcnv  29037  f1ocan2fv  30218  isdrngo2  30361  eluzrabdioph  30739  iocmbl  31180  lcmgcdeq  31216  dvconstbi  31239  sinhpcosh  33134  reseccl  33147  recsccl  33148  recotcl  33149  onetansqsecsq  33155  eelT11  33496  eelT12  33500  eelTT1  33502  eel0T1  33504  atncvrN  35040  cvlatcvr1  35066  rp-isfinite6  37744
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975
  Copyright terms: Public domain W3C validator