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

Theorem simpri 477
 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 476 . 2 ((𝜑𝜓) → 𝜓)
31, 2ax-mp 5 1 𝜓
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 383 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 197  df-an 385 This theorem is referenced by:  exan  1828  exanOLD  1829  exanOLDOLD  2205  tfr2b  7537  rdgdmlim  7558  oeoa  7722  oeoe  7724  ordtypelem3  8466  ordtypelem5  8468  ordtypelem6  8469  ordtypelem7  8470  ordtypelem9  8472  r1fin  8674  r1tr  8677  r1ordg  8679  r1ord3g  8680  r1pwss  8685  r1val1  8687  rankwflemb  8694  r1elwf  8697  rankr1ai  8699  rankdmr1  8702  rankr1ag  8703  rankr1bg  8704  pwwf  8708  unwf  8711  rankr1clem  8721  rankr1c  8722  rankval3b  8727  rankonidlem  8729  onssr1  8732  rankeq0b  8761  alephsuc2  8941  ackbij2  9103  wunom  9580  negiso  11041  infrenegsup  11044  om2uzoi  12794  faclbnd4lem1  13120  hashunlei  13250  hashsslei  13251  hashle2pr  13297  cos01bnd  14960  cos1bnd  14961  cos2bnd  14962  sincos2sgn  14968  sin4lt0  14969  egt2lt3  14978  divalglem9  15171  bitsinv  15217  strlemor1OLD  16016  drngui  18801  redvr  20011  refld  20013  recrng  20015  iccpnfcnv  22790  xrhmph  22793  recvs  22992  qcvs  22993  i1f1  23502  itg11  23503  dvcos  23791  sinpi  24254  sinhalfpilem  24260  coshalfpi  24266  sincosq1lem  24294  tangtx  24302  sincos4thpi  24310  tan4thpi  24311  sincos6thpi  24312  sincos3rdpi  24313  pige3  24314  logltb  24391  1cubrlem  24613  1cubr  24614  log2tlbnd  24717  cxploglim2  24750  emcllem6  24772  emcllem7  24773  ppiublem1  24972  ppiublem2  24973  bposlem9  25062  lgsdir2lem4  25098  lgsdir2lem5  25099  chebbnd1lem2  25204  chebbnd1lem3  25205  chebbnd1  25206  dchrvmasumlema  25234  mulog2sumlem2  25269  pntlemb  25331  qdrng  25354  upgrbi  26033  upgr1elem  26052  usgrexmpledg  26199  ntrl2v2e  27136  frgrwopreg2  27299  normlem7tALT  28104  hhsssh  28254  shintcli  28316  chintcli  28318  omlsi  28391  qlaxr3i  28623  lnophm  29006  nmcopex  29016  nmcoplb  29017  nmbdfnlbi  29036  nmcfnex  29040  nmcfnlb  29041  hmopidmch  29140  hmopidmpj  29141  chirred  29382  xrge0hmph  30106  qqh0  30156  qqh1  30157  rerrext  30181  zrhre  30191  qqhre  30192  mbfmvolf  30456  hgt750lem  30857  subfacval2  31295  erdszelem5  31303  erdszelem6  31304  erdszelem7  31305  erdszelem8  31306  filnetlem3  32500  filnetlem4  32501  bj-genr  32716  bj-genl  32717  bj-genan  32718  uun0.1  39322  pssnssi  39597  fourierdlem62  40703  fourierdlem68  40709  abcdtb  41414  abcdtc  41415  abcdtd  41416  nabctnabc  41419  zlmodzxzsubm  42462  zlmodzxzldep  42618  ldepsnlinclem1  42619  ldepsnlinclem2  42620
 Copyright terms: Public domain W3C validator