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

Theorem simpli 460
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 459 . 2  |-  ( (
ph  /\  ps )  ->  ph )
31, 2ax-mp 5 1  |-  ph
Colors of variables: wff setvar class
Syntax hints:    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  pwundif  4744  tfr2b  7119  rdgfun  7139  oeoa  7303  oeoe  7305  ssdomg  7620  ordtypelem4  8041  ordtypelem6  8043  ordtypelem7  8044  r1limg  8247  rankwflemb  8269  r1elssi  8281  infxpenlem  8449  ackbij2  8678  wunom  9150  mulnzcnopr  10265  negiso  10594  infrenegsup  10598  infmsupOLD  10599  hashunlei  12604  hashsslei  12605  cos01bnd  14252  cos1bnd  14253  cos2bnd  14254  sin4lt0  14261  egt2lt3  14270  epos  14271  ene1  14274  divalglem5OLD  14388  divalglem5  14389  bitsf1o  14431  gcdaddmlem  14504  strlemor1  15229  zrhpsgnmhm  19164  resubgval  19189  re1r  19193  redvr  19197  refld  19199  txindis  20661  icopnfhmeo  21983  iccpnfcnv  21984  iccpnfhmeo  21985  xrhmeo  21986  cnheiborlem  21994  rrxcph  22363  volf  22495  i1f1  22660  itg11  22661  dvsin  22946  taylthlem2  23341  reefgim  23417  pilem3  23421  pilem3OLD  23422  pigt2lt4  23423  pire  23425  pipos  23427  sinhalfpi  23435  tan4thpi  23481  sincos3rdpi  23483  circgrp  23513  circsubm  23514  rzgrp  23515  1cubrlem  23779  1cubr  23780  jensenlem2  23925  amgmlem  23927  emcllem6  23938  emcllem7  23939  emgt0  23944  harmonicbnd3  23945  ppiublem1  24142  chtub  24152  bposlem7  24230  lgsdir2lem4  24266  lgsdir2lem5  24267  chebbnd1  24322  mulog2sumlem2  24385  pntpbnd1a  24435  pntpbnd2  24437  pntlemb  24447  pntlemk  24456  qrng0  24471  qrng1  24472  qrngneg  24473  qrngdiv  24474  qabsabv  24479  2trllemE  25295  normlem7tALT  26784  hhsssh  26932  shintcli  26994  chintcli  26996  omlsi  27069  qlaxr3i  27301  lnophm  27684  nmcopex  27694  nmcoplb  27695  nmbdfnlbi  27714  nmcfnex  27718  nmcfnlb  27719  hmopidmch  27818  hmopidmpj  27819  chirred  28060  nn0archi  28618  xrge0iifiso  28753  xrge0iifmhm  28757  xrge0pluscn  28758  rezh  28787  qqh0  28800  qqh1  28801  qqhcn  28807  qqhucn  28808  rerrext  28825  cnrrext  28826  mbfmvolf  29100  subfacval3  29924  erdszelem5  29930  erdszelem8  29933  ghomgrpilem2  30316  filnetlem3  31048  filnetlem4  31049  pigt3  31950  reheibor  32183  fourierdlem68  38048  fourierdlem77  38057  fourierdlem80  38060  fouriersw  38105  etransclem23  38132  gsumge0cl  38223  abcdta  38523  abcdtb  38524  abcdtc  38525  nabctnabc  38529  zlmodzxzsubm  40244  zlmodzxzldeplem3  40399  ldepsnlinclem1  40402  ldepsnlinclem2  40403  ldepsnlinc  40405  empty-surprise  40625
  Copyright terms: Public domain W3C validator