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

Theorem simpli 455
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 454 . 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  4615  tfr2b  6841  rdgfun  6858  oeoa  7024  oeoe  7026  ssdomg  7343  ordtypelem4  7723  ordtypelem6  7725  ordtypelem7  7726  r1limg  7966  rankwflemb  7988  r1elssi  8000  infxpenlem  8168  ackbij2  8400  wunom  8874  mulnzcnopr  9969  negiso  10293  infmsup  10295  hashunlei  12158  hashsslei  12159  cos01bnd  13452  cos1bnd  13453  cos2bnd  13454  sin4lt0  13461  egt2lt3  13470  epos  13471  divalglem5  13583  bitsf1o  13623  gcdaddmlem  13694  strlemor1  14247  zrhpsgnmhm  17855  resubgval  17880  re1r  17884  redvr  17888  refld  17890  txindis  19048  icopnfhmeo  20356  iccpnfcnv  20357  iccpnfhmeo  20358  xrhmeo  20359  cnheiborlem  20367  rrxcph  20737  volf  20853  i1f1  21009  itg11  21010  dvsin  21295  taylthlem2  21723  reefgim  21799  pilem3  21802  pigt2lt4  21803  pire  21805  pipos  21807  sinhalfpi  21814  tan4thpi  21860  sincos3rdpi  21862  1cubrlem  22120  1cubr  22121  jensenlem2  22265  amgmlem  22267  emcllem6  22278  emcllem7  22279  emgt0  22284  harmonicbnd3  22285  ppiublem1  22425  chtub  22435  bposlem7  22513  lgsdir2lem4  22549  lgsdir2lem5  22550  chebbnd1  22605  mulog2sumlem2  22668  pntpbnd1a  22718  pntpbnd2  22720  pntlemb  22730  pntlemk  22739  qrng0  22754  qrng1  22755  qrngneg  22756  qrngdiv  22757  qabsabv  22762  2trllemE  23274  normlem7tALT  24343  hhsssh  24492  shintcli  24554  chintcli  24556  omlsi  24629  qlaxr3i  24861  lnophm  25245  nmcopex  25255  nmcoplb  25256  nmbdfnlbi  25275  nmcfnex  25279  nmcfnlb  25280  hmopidmch  25379  hmopidmpj  25380  chirred  25621  nn0archi  26164  xrge0iifiso  26218  xrge0iifmhm  26222  xrge0pluscn  26223  rezh  26253  qqh0  26266  qqh1  26267  qqhcn  26273  qqhucn  26274  rerrext  26291  cnrrext  26292  mbfmvolf  26534  subfacval3  26924  erdszelem5  26930  erdszelem8  26933  ghomgrpilem2  27151  filnetlem3  28442  filnetlem4  28443  reheibor  28579  abcdta  29779  abcdtb  29780  abcdtc  29781  zlmodzxzsubm  30587  zlmodzxzldeplem3  30750  ldepsnlinclem1  30753  ldepsnlinclem2  30754  ldepsnlinc  30756  ene1  30815  empty-surprise  30838  bj-pirp  32105  pirp  35183
  Copyright terms: Public domain W3C validator