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

Theorem simpli 456
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 455 . 2  |-  ( (
ph  /\  ps )  ->  ph )
31, 2ax-mp 5 1  |-  ph
Colors of variables: wff setvar class
Syntax hints:    /\ wa 367
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 369
This theorem is referenced by:  pwundif  4701  tfr2b  6983  rdgfun  7000  oeoa  7164  oeoe  7166  ssdomg  7480  ordtypelem4  7861  ordtypelem6  7863  ordtypelem7  7864  r1limg  8102  rankwflemb  8124  r1elssi  8136  infxpenlem  8304  ackbij2  8536  wunom  9009  mulnzcnopr  10112  negiso  10435  infmsup  10437  hashunlei  12387  hashsslei  12388  cos01bnd  13923  cos1bnd  13924  cos2bnd  13925  sin4lt0  13932  egt2lt3  13941  epos  13942  ene1  13945  divalglem5  14057  bitsf1o  14097  gcdaddmlem  14168  strlemor1  14729  zrhpsgnmhm  18711  resubgval  18736  re1r  18740  redvr  18744  refld  18746  txindis  20220  icopnfhmeo  21528  iccpnfcnv  21529  iccpnfhmeo  21530  xrhmeo  21531  cnheiborlem  21539  rrxcph  21909  volf  22025  i1f1  22182  itg11  22183  dvsin  22468  taylthlem2  22854  reefgim  22930  pilem3  22933  pigt2lt4  22934  pire  22936  pipos  22938  sinhalfpi  22946  tan4thpi  22992  sincos3rdpi  22994  circgrp  23024  circsubm  23025  rzgrp  23026  1cubrlem  23288  1cubr  23289  jensenlem2  23434  amgmlem  23436  emcllem6  23447  emcllem7  23448  emgt0  23453  harmonicbnd3  23454  ppiublem1  23594  chtub  23604  bposlem7  23682  lgsdir2lem4  23718  lgsdir2lem5  23719  chebbnd1  23774  mulog2sumlem2  23837  pntpbnd1a  23887  pntpbnd2  23889  pntlemb  23899  pntlemk  23908  qrng0  23923  qrng1  23924  qrngneg  23925  qrngdiv  23926  qabsabv  23931  2trllemE  24676  normlem7tALT  26153  hhsssh  26302  shintcli  26364  chintcli  26366  omlsi  26439  qlaxr3i  26671  lnophm  27054  nmcopex  27064  nmcoplb  27065  nmbdfnlbi  27084  nmcfnex  27088  nmcfnlb  27089  hmopidmch  27188  hmopidmpj  27189  chirred  27430  nn0archi  27987  xrge0iifiso  28071  xrge0iifmhm  28075  xrge0pluscn  28076  rezh  28105  qqh0  28118  qqh1  28119  qqhcn  28125  qqhucn  28126  rerrext  28143  cnrrext  28144  mbfmvolf  28393  subfacval3  28822  erdszelem5  28828  erdszelem8  28831  ghomgrpilem2  29215  filnetlem3  30364  filnetlem4  30365  reheibor  30501  fourierdlem68  32123  fourierdlem77  32132  fourierdlem80  32135  fouriersw  32180  etransclem23  32206  abcdta  32283  abcdtb  32284  abcdtc  32285  zlmodzxzsubm  33148  zlmodzxzldeplem3  33303  ldepsnlinclem1  33306  ldepsnlinclem2  33307  ldepsnlinc  33309  empty-surprise  33531
  Copyright terms: Public domain W3C validator