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

Theorem simpli 472
Description: Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.)
Hypothesis
Ref Expression
simpli.1 (𝜑𝜓)
Assertion
Ref Expression
simpli 𝜑

Proof of Theorem simpli
StepHypRef Expression
1 simpli.1 . 2 (𝜑𝜓)
2 simpl 470 . 2 ((𝜑𝜓) → 𝜑)
31, 2ax-mp 5 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wa 384
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 198  df-an 385
This theorem is referenced by:  exan  1948  exanOLD  1949  pwundif  5223  tfr2b  7731  rdgfun  7751  oeoa  7917  oeoe  7919  ssdomg  8241  ordtypelem4  8668  ordtypelem6  8670  ordtypelem7  8671  r1limg  8884  rankwflemb  8906  r1elssi  8918  infxpenlem  9122  ackbij2  9353  wunom  9830  mulnzcnopr  10961  negiso  11291  infrenegsup  11294  hashunlei  13432  hashsslei  13433  cos01bnd  15139  cos1bnd  15140  cos2bnd  15141  sin4lt0  15148  egt2lt3  15157  epos  15158  ene1  15161  divalglem5  15343  bitsf1o  15389  gcdaddmlem  15467  strlemor1OLD  16183  zrhpsgnmhm  20140  resubgval  20167  re1r  20171  redvr  20175  refld  20177  rzgrp  20181  txindis  21655  icopnfhmeo  22959  iccpnfcnv  22960  iccpnfhmeo  22961  xrhmeo  22962  cnheiborlem  22970  recvs  23162  qcvs  23163  rrxcph  23398  volf  23516  i1f1  23677  itg11  23678  dvsin  23965  taylthlem2  24348  reefgim  24424  pilem3  24427  pilem3OLD  24428  pigt2lt4  24429  pire  24431  pipos  24433  sinhalfpi  24441  tan4thpi  24487  sincos3rdpi  24489  circgrp  24519  circsubm  24520  1cubrlem  24788  1cubr  24789  jensenlem2  24934  amgmlem  24936  emcllem6  24947  emcllem7  24948  emgt0  24953  harmonicbnd3  24954  ppiublem1  25147  chtub  25157  bposlem7  25235  lgsdir2lem4  25273  lgsdir2lem5  25274  chebbnd1  25381  mulog2sumlem2  25444  pntpbnd1a  25494  pntpbnd2  25496  pntlemb  25506  pntlemk  25515  qrng0  25530  qrng1  25531  qrngneg  25532  qrngdiv  25533  qabsabv  25538  ex-sqrt  27648  normlem7tALT  28310  hhsssh  28460  shintcli  28522  chintcli  28524  omlsi  28597  qlaxr3i  28829  lnophm  29212  nmcopex  29222  nmcoplb  29223  nmbdfnlbi  29242  nmcfnex  29246  nmcfnlb  29247  hmopidmch  29346  hmopidmpj  29347  chirred  29588  threehalves  29954  nn0archi  30174  xrge0iifiso  30312  xrge0iifmhm  30316  xrge0pluscn  30317  rezh  30346  qqh0  30359  qqh1  30360  qqhcn  30366  qqhucn  30367  rerrext  30384  cnrrext  30385  mbfmvolf  30659  hgt750lem  31060  subfacval3  31499  erdszelem5  31505  erdszelem8  31508  filnetlem3  32701  filnetlem4  32702  bj-genr  32911  bj-genl  32912  bj-genan  32913  pigt3  33717  reheibor  33951  cossssid  34532  fourierdlem68  40871  fourierdlem77  40880  fourierdlem80  40883  fouriersw  40928  etransclem23  40954  gsumge0cl  41068  abcdta  41575  abcdtb  41576  abcdtc  41577  nabctnabc  41581  zlmodzxzsubm  42706  zlmodzxzldeplem3  42860  ldepsnlinclem1  42863  ldepsnlinclem2  42864  ldepsnlinc  42866  empty-surprise  43100  amgmwlem  43120  amgmlemALT  43121
  Copyright terms: Public domain W3C validator