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

Theorem simpri 462
Description: Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.)
Hypothesis
Ref Expression
simpri.1
Assertion
Ref Expression
simpri

Proof of Theorem simpri
StepHypRef Expression
1 simpri.1 . 2
2 simpr 461 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  /\wa 369
This theorem is referenced by:  exan  1973  tfr2b  7084  rdgdmlim  7102  oeoa  7265  oeoe  7267  ordtypelem3  7966  ordtypelem5  7968  ordtypelem6  7969  ordtypelem7  7970  ordtypelem9  7972  r1fin  8212  r1tr  8215  r1ordg  8217  r1ord3g  8218  r1pwss  8223  r1val1  8225  rankwflemb  8232  r1elwf  8235  rankr1ai  8237  rankdmr1  8240  rankr1ag  8241  rankr1bg  8242  pwwf  8246  unwf  8249  rankr1clem  8259  rankr1c  8260  rankval3b  8265  rankonidlem  8267  onssr1  8270  rankeq0b  8299  alephsuc2  8482  ackbij2  8644  wunom  9119  negiso  10544  infmsup  10546  om2uzoi  12066  faclbnd4lem1  12371  hashgt12el  12481  hashgt12el2  12482  hashunlei  12483  hashsslei  12484  cos01bnd  13921  cos1bnd  13922  cos2bnd  13923  sincos2sgn  13929  sin4lt0  13930  egt2lt3  13939  divalglem9  14059  bitsinv  14098  strlemor1  14724  drngui  17402  redvr  18653  refld  18655  recrng  18657  iccpnfcnv  21444  xrhmph  21447  i1f1  22097  itg11  22098  dvcos  22384  sinpi  22850  sinhalfpilem  22856  coshalfpi  22862  sincosq1lem  22890  tangtx  22898  sincos4thpi  22906  tan4thpi  22907  sincos6thpi  22908  sincos3rdpi  22909  pige3  22910  logltb  22984  1cubrlem  23172  1cubr  23173  log2tlbnd  23276  cxploglim2  23308  emcllem6  23330  emcllem7  23331  ppiublem1  23477  ppiublem2  23478  bposlem9  23567  lgsdir2lem4  23601  lgsdir2lem5  23602  chebbnd1lem2  23655  chebbnd1lem3  23656  chebbnd1  23657  dchrvmasumlema  23685  mulog2sumlem2  23720  pntlemb  23782  qdrng  23805  umgra1  24326  uslgra1  24372  2trllemE  24555  umgrabi  24983  normlem7tALT  26036  hhsssh  26185  shintcli  26247  chintcli  26249  omlsi  26322  qlaxr3i  26554  lnophm  26938  nmcopex  26948  nmcoplb  26949  nmbdfnlbi  26968  nmcfnex  26972  nmcfnlb  26973  hmopidmch  27072  hmopidmpj  27073  chirred  27314  xrge0hmph  27914  qqh0  27965  qqh1  27966  rerrext  27990  zrhre  27997  qqhre  27998  mbfmvolf  28237  subfacval2  28631  erdszelem5  28639  erdszelem6  28640  erdszelem7  28641  erdszelem8  28642  ghomgrpilem1  29025  filnetlem3  30198  filnetlem4  30199  fourierdlem62  31951  fourierdlem68  31957  abcdtb  32118  abcdtc  32119  abcdtd  32120  zlmodzxzsubm  32948  zlmodzxzldep  33105  ldepsnlinclem1  33106  ldepsnlinclem2  33107  uun0.1  33575
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
  Copyright terms: Public domain W3C validator