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

Theorem simpli 458
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 457 . 2  |-  ( (
ph  /\  ps )  ->  ph )
31, 2ax-mp 5 1  |-  ph
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  pwundif  4627  tfr2b  6854  rdgfun  6871  oeoa  7035  oeoe  7037  ssdomg  7354  ordtypelem4  7734  ordtypelem6  7736  ordtypelem7  7737  r1limg  7977  rankwflemb  7999  r1elssi  8011  infxpenlem  8179  ackbij2  8411  wunom  8886  mulnzcnopr  9981  negiso  10305  infmsup  10307  hashunlei  12174  hashsslei  12175  cos01bnd  13469  cos1bnd  13470  cos2bnd  13471  sin4lt0  13478  egt2lt3  13487  epos  13488  divalglem5  13600  bitsf1o  13640  gcdaddmlem  13711  strlemor1  14264  zrhpsgnmhm  18013  resubgval  18038  re1r  18042  redvr  18046  refld  18048  txindis  19206  icopnfhmeo  20514  iccpnfcnv  20515  iccpnfhmeo  20516  xrhmeo  20517  cnheiborlem  20525  rrxcph  20895  volf  21011  i1f1  21167  itg11  21168  dvsin  21453  taylthlem2  21838  reefgim  21914  pilem3  21917  pigt2lt4  21918  pire  21920  pipos  21922  sinhalfpi  21929  tan4thpi  21975  sincos3rdpi  21977  1cubrlem  22235  1cubr  22236  jensenlem2  22380  amgmlem  22382  emcllem6  22393  emcllem7  22394  emgt0  22399  harmonicbnd3  22400  ppiublem1  22540  chtub  22550  bposlem7  22628  lgsdir2lem4  22664  lgsdir2lem5  22665  chebbnd1  22720  mulog2sumlem2  22783  pntpbnd1a  22833  pntpbnd2  22835  pntlemb  22845  pntlemk  22854  qrng0  22869  qrng1  22870  qrngneg  22871  qrngdiv  22872  qabsabv  22877  2trllemE  23451  normlem7tALT  24520  hhsssh  24669  shintcli  24731  chintcli  24733  omlsi  24806  qlaxr3i  25038  lnophm  25422  nmcopex  25432  nmcoplb  25433  nmbdfnlbi  25452  nmcfnex  25456  nmcfnlb  25457  hmopidmch  25556  hmopidmpj  25557  chirred  25798  nn0archi  26310  xrge0iifiso  26364  xrge0iifmhm  26368  xrge0pluscn  26369  rezh  26399  qqh0  26412  qqh1  26413  qqhcn  26419  qqhucn  26420  rerrext  26437  cnrrext  26438  mbfmvolf  26680  subfacval3  27076  erdszelem5  27082  erdszelem8  27085  ghomgrpilem2  27304  filnetlem3  28599  filnetlem4  28600  reheibor  28736  abcdta  29934  abcdtb  29935  abcdtc  29936  zlmodzxzsubm  30754  zlmodzxzldeplem3  31042  ldepsnlinclem1  31045  ldepsnlinclem2  31046  ldepsnlinc  31048  ene1  31107  empty-surprise  31132  bj-pirp  32526  pirp  35611
  Copyright terms: Public domain W3C validator