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

Theorem simpli 465
Description: Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.)
Hypothesis
Ref Expression
simpli.1  |-  ( ph  /\ 
ps )
Assertion
Ref Expression
simpli  |-  ph

Proof of Theorem simpli
StepHypRef Expression
1 simpli.1 . 2  |-  ( ph  /\ 
ps )
2 simpl 464 . 2  |-  ( (
ph  /\  ps )  ->  ph )
31, 2ax-mp 5 1  |-  ph
Colors of variables: wff setvar class
Syntax hints:    /\ wa 376
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 190  df-an 378
This theorem is referenced by:  pwundif  4746  tfr2b  7132  rdgfun  7152  oeoa  7316  oeoe  7318  ssdomg  7633  ordtypelem4  8054  ordtypelem6  8056  ordtypelem7  8057  r1limg  8260  rankwflemb  8282  r1elssi  8294  infxpenlem  8462  ackbij2  8691  wunom  9163  mulnzcnopr  10280  negiso  10609  infrenegsup  10613  infmsupOLD  10614  hashunlei  12638  hashsslei  12639  cos01bnd  14317  cos1bnd  14318  cos2bnd  14319  sin4lt0  14326  egt2lt3  14335  epos  14336  ene1  14339  divalglem5OLD  14455  divalglem5  14456  bitsf1o  14498  gcdaddmlem  14571  strlemor1  15295  zrhpsgnmhm  19229  resubgval  19254  re1r  19258  redvr  19262  refld  19264  txindis  20726  icopnfhmeo  22049  iccpnfcnv  22050  iccpnfhmeo  22051  xrhmeo  22052  cnheiborlem  22060  rrxcph  22429  volf  22561  i1f1  22727  itg11  22728  dvsin  23013  taylthlem2  23408  reefgim  23484  pilem3  23488  pilem3OLD  23489  pigt2lt4  23490  pire  23492  pipos  23494  sinhalfpi  23502  tan4thpi  23548  sincos3rdpi  23550  circgrp  23580  circsubm  23581  rzgrp  23582  1cubrlem  23846  1cubr  23847  jensenlem2  23992  amgmlem  23994  emcllem6  24005  emcllem7  24006  emgt0  24011  harmonicbnd3  24012  ppiublem1  24209  chtub  24219  bposlem7  24297  lgsdir2lem4  24333  lgsdir2lem5  24334  chebbnd1  24389  mulog2sumlem2  24452  pntpbnd1a  24502  pntpbnd2  24504  pntlemb  24514  pntlemk  24523  qrng0  24538  qrng1  24539  qrngneg  24540  qrngdiv  24541  qabsabv  24546  2trllemE  25362  normlem7tALT  26853  hhsssh  27001  shintcli  27063  chintcli  27065  omlsi  27138  qlaxr3i  27370  lnophm  27753  nmcopex  27763  nmcoplb  27764  nmbdfnlbi  27783  nmcfnex  27787  nmcfnlb  27788  hmopidmch  27887  hmopidmpj  27888  chirred  28129  nn0archi  28680  xrge0iifiso  28815  xrge0iifmhm  28819  xrge0pluscn  28820  rezh  28849  qqh0  28862  qqh1  28863  qqhcn  28869  qqhucn  28870  rerrext  28887  cnrrext  28888  mbfmvolf  29161  subfacval3  29984  erdszelem5  29990  erdszelem8  29993  ghomgrpilem2  30376  filnetlem3  31107  filnetlem4  31108  pigt3  32002  reheibor  32235  fourierdlem68  38150  fourierdlem77  38159  fourierdlem80  38162  fouriersw  38207  etransclem23  38234  gsumge0cl  38327  abcdta  38658  abcdtb  38659  abcdtc  38660  nabctnabc  38664  zlmodzxzsubm  40648  zlmodzxzldeplem3  40803  ldepsnlinclem1  40806  ldepsnlinclem2  40807  ldepsnlinc  40809  empty-surprise  41027
  Copyright terms: Public domain W3C validator