MPE Home 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 196  df-an 385
This theorem is referenced by:  exan  1775  exanOLD  1776  exanOLDOLD  2155  tfr2b  7357  rdgdmlim  7378  oeoa  7542  oeoe  7544  ordtypelem3  8286  ordtypelem5  8288  ordtypelem6  8289  ordtypelem7  8290  ordtypelem9  8292  r1fin  8497  r1tr  8500  r1ordg  8502  r1ord3g  8503  r1pwss  8508  r1val1  8510  rankwflemb  8517  r1elwf  8520  rankr1ai  8522  rankdmr1  8525  rankr1ag  8526  rankr1bg  8527  pwwf  8531  unwf  8534  rankr1clem  8544  rankr1c  8545  rankval3b  8550  rankonidlem  8552  onssr1  8555  rankeq0b  8584  alephsuc2  8764  ackbij2  8926  wunom  9399  negiso  10853  infrenegsup  10856  om2uzoi  12574  faclbnd4lem1  12900  hashunlei  13027  hashsslei  13028  cos01bnd  14704  cos1bnd  14705  cos2bnd  14706  sincos2sgn  14712  sin4lt0  14713  egt2lt3  14722  divalglem9  14911  bitsinv  14957  strlemor1  15745  drngui  18525  redvr  19730  refld  19732  recrng  19734  iccpnfcnv  22499  xrhmph  22502  i1f1  23208  itg11  23209  dvcos  23495  sinpi  23958  sinhalfpilem  23964  coshalfpi  23970  sincosq1lem  23998  tangtx  24006  sincos4thpi  24014  tan4thpi  24015  sincos6thpi  24016  sincos3rdpi  24017  pige3  24018  logltb  24095  1cubrlem  24313  1cubr  24314  log2tlbnd  24417  cxploglim2  24450  emcllem6  24472  emcllem7  24473  ppiublem1  24672  ppiublem2  24673  bposlem9  24762  lgsdir2lem4  24798  lgsdir2lem5  24799  chebbnd1lem2  24904  chebbnd1lem3  24905  chebbnd1  24906  dchrvmasumlema  24934  mulog2sumlem2  24969  pntlemb  25031  qdrng  25054  umgra1  25649  uslgra1  25695  2trllemE  25877  umgrabi  26304  normlem7tALT  27154  hhsssh  27304  shintcli  27366  chintcli  27368  omlsi  27441  qlaxr3i  27673  lnophm  28056  nmcopex  28066  nmcoplb  28067  nmbdfnlbi  28086  nmcfnex  28090  nmcfnlb  28091  hmopidmch  28190  hmopidmpj  28191  chirred  28432  xrge0hmph  29100  qqh0  29150  qqh1  29151  rerrext  29175  zrhre  29185  qqhre  29186  mbfmvolf  29449  subfacval2  30217  erdszelem5  30225  erdszelem6  30226  erdszelem7  30227  erdszelem8  30228  filnetlem3  31339  filnetlem4  31340  bj-genr  31570  bj-genl  31571  bj-genan  31572  uun0.1  37820  pssnssi  38106  fourierdlem62  38855  fourierdlem68  38861  abcdtb  39536  abcdtc  39537  abcdtd  39538  nabctnabc  39541  upgrbi  40311  upgr1elem  40329  usgrexmpledg  40478  ntrl2v2e  41317  frgrwopreg2  41480  zlmodzxzsubm  41922  zlmodzxzldep  42079  ldepsnlinclem1  42080  ldepsnlinclem2  42081
  Copyright terms: Public domain W3C validator