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

Theorem simpli 444
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 443 . 2  |-  ( (
ph  /\  ps )  ->  ph )
31, 2ax-mp 8 1  |-  ph
Colors of variables: wff set class
Syntax hints:    /\ wa 358
This theorem is referenced by:  pwundif  4316  tfr2b  6428  rdgfun  6445  oeoa  6611  oeoe  6613  ssdomg  6923  ordtypelem4  7252  ordtypelem6  7254  ordtypelem7  7255  r1limg  7459  rankwflemb  7481  r1elssi  7493  infxpenlem  7657  ackbij2  7885  wunom  8358  mulnzcnopr  9430  negiso  9746  infmsup  9748  hashunlei  11393  hashsslei  11394  cos01bnd  12482  cos1bnd  12483  cos2bnd  12484  sin4lt0  12491  egt2lt3  12500  epos  12501  divalglem5  12612  bitsf1o  12652  gcdaddmlem  12723  strlemor1  13251  txindis  17344  icopnfhmeo  18457  iccpnfcnv  18458  iccpnfhmeo  18459  xrhmeo  18460  cnheiborlem  18468  volf  18904  i1f1  19061  itg11  19062  dvsin  19345  taylthlem2  19769  reefgim  19842  pilem3  19845  pigt2lt4  19846  pire  19848  pipos  19849  sinhalfpi  19852  tan4thpi  19898  sincos3rdpi  19900  1cubrlem  20153  1cubr  20154  jensenlem2  20298  amgmlem  20300  emcllem6  20310  emcllem7  20311  emgt0  20316  harmonicbnd3  20317  ppiublem1  20457  chtub  20467  bposlem7  20545  lgsdir2lem4  20581  lgsdir2lem5  20582  chebbnd1  20637  mulog2sumlem2  20700  pntpbnd1a  20750  pntpbnd2  20752  pntlemb  20762  pntlemk  20771  qrng0  20786  qrng1  20787  qrngneg  20788  qrngdiv  20789  qabsabv  20794  normlem7tALT  21714  hhsssh  21862  shintcli  21924  chintcli  21926  omlsi  21999  qlaxr3i  22231  lnophm  22615  nmcopex  22625  nmcoplb  22626  nmbdfnlbi  22645  nmcfnex  22649  nmcfnlb  22650  hmopidmch  22749  hmopidmpj  22750  chirred  22991  pwundif2  23202  xrge0iifiso  23332  xrge0iifmhm  23336  xrge0pluscn  23337  mbfmvolf  23586  subfacval3  23735  erdszelem5  23741  erdszelem8  23744  ghomgrpilem2  24008  cntrset  25705  pvp  26151  filnetlem3  26432  filnetlem4  26433  reheibor  26666  ene1  28512
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator