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

Theorem simpli 487
 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 486 . 2 ((𝜑𝜓) → 𝜑)
31, 2ax-mp 5 1 𝜑
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  pwundifOLD  5422  tfr2b  8017  rdgfun  8037  oeoa  8208  oeoe  8210  ssdomg  8540  ordtypelem4  8971  ordtypelem6  8973  ordtypelem7  8974  r1limg  9186  rankwflemb  9208  r1elssi  9220  infxpenlem  9426  ackbij2  9656  wunom  10133  mulnzcnopr  11277  negiso  11610  infrenegsup  11613  hashunlei  13784  hashsslei  13785  cos01bnd  15533  cos1bnd  15534  cos2bnd  15535  sin4lt0  15542  egt2lt3  15553  epos  15554  ene1  15557  divalglem5  15740  bitsf1o  15786  gcdaddmlem  15864  zrhpsgnmhm  20277  resubgval  20302  re1r  20306  redvr  20310  refld  20312  rzgrp  20316  txindis  22246  icopnfhmeo  23555  iccpnfcnv  23556  iccpnfhmeo  23557  xrhmeo  23558  cnheiborlem  23566  recvs  23758  qcvs  23759  rrxcph  24003  volf  24140  i1f1  24301  itg11  24302  dvsin  24592  taylthlem2  24976  reefgim  25052  pilem3  25055  pigt2lt4  25056  pire  25058  pipos  25060  sinhalfpi  25068  tan4thpi  25114  sincos3rdpi  25116  pigt3  25117  circgrp  25151  circsubm  25152  1cubrlem  25434  1cubr  25435  jensenlem2  25580  amgmlem  25582  emcllem6  25593  emcllem7  25594  harmonicbnd3  25600  ppiublem1  25793  chtub  25803  bposlem7  25881  lgsdir2lem4  25919  lgsdir2lem5  25920  chebbnd1  26063  mulog2sumlem2  26126  pntpbnd1a  26176  pntpbnd2  26178  pntlemb  26188  pntlemk  26197  qrng0  26212  qrng1  26213  qrngneg  26214  qrngdiv  26215  qabsabv  26220  ex-sqrt  28246  normlem7tALT  28909  hhsssh  29059  shintcli  29119  chintcli  29121  omlsi  29194  qlaxr3i  29426  lnophm  29809  nmcopex  29819  nmcoplb  29820  nmbdfnlbi  29839  nmcfnex  29843  nmcfnlb  29844  hmopidmch  29943  hmopidmpj  29944  chirred  30185  threehalves  30624  nn0archi  30974  ccfldextrr  31138  ccfldsrarelvec  31156  xrge0iifiso  31300  xrge0iifmhm  31304  xrge0pluscn  31305  rezh  31334  qqh0  31347  qqh1  31348  qqhcn  31354  qqhucn  31355  rerrext  31372  cnrrext  31373  mbfmvolf  31646  hgt750lem  32044  subfacval3  32561  erdszelem5  32567  erdszelem8  32570  filnetlem3  33853  filnetlem4  33854  bj-genr  34069  bj-genl  34070  bj-genan  34071  bj-rveccmod  34732  reheibor  35293  cossssid  35883  eqvrelcoss3  36029  fourierdlem68  42831  fourierdlem77  42840  fourierdlem80  42843  fouriersw  42888  etransclem23  42914  gsumge0cl  43025  abcdta  43533  abcdtb  43534  abcdtc  43535  nabctnabc  43539  zlmodzxzsubm  44776  zlmodzxzldeplem3  44925  ldepsnlinclem1  44928  ldepsnlinclem2  44929  ldepsnlinc  44931  empty-surprise  45324  amgmwlem  45344  amgmlemALT  45345
 Copyright terms: Public domain W3C validator