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  4793  tfr2b  7077  rdgfun  7094  oeoa  7258  oeoe  7260  ssdomg  7573  ordtypelem4  7958  ordtypelem6  7960  ordtypelem7  7961  r1limg  8201  rankwflemb  8223  r1elssi  8235  infxpenlem  8403  ackbij2  8635  wunom  9110  mulnzcnopr  10207  negiso  10531  infmsup  10533  hashunlei  12463  hashsslei  12464  cos01bnd  13799  cos1bnd  13800  cos2bnd  13801  sin4lt0  13808  egt2lt3  13817  epos  13818  divalglem5  13931  bitsf1o  13971  gcdaddmlem  14042  strlemor1  14599  zrhpsgnmhm  18489  resubgval  18514  re1r  18518  redvr  18522  refld  18524  txindis  20003  icopnfhmeo  21311  iccpnfcnv  21312  iccpnfhmeo  21313  xrhmeo  21314  cnheiborlem  21322  rrxcph  21692  volf  21808  i1f1  21965  itg11  21966  dvsin  22251  taylthlem2  22636  reefgim  22712  pilem3  22715  pigt2lt4  22716  pire  22718  pipos  22720  sinhalfpi  22727  tan4thpi  22773  sincos3rdpi  22775  circgrp  22805  circsubm  22806  rzgrp  22807  1cubrlem  23038  1cubr  23039  jensenlem2  23183  amgmlem  23185  emcllem6  23196  emcllem7  23197  emgt0  23202  harmonicbnd3  23203  ppiublem1  23343  chtub  23353  bposlem7  23431  lgsdir2lem4  23467  lgsdir2lem5  23468  chebbnd1  23523  mulog2sumlem2  23586  pntpbnd1a  23636  pntpbnd2  23638  pntlemb  23648  pntlemk  23657  qrng0  23672  qrng1  23673  qrngneg  23674  qrngdiv  23675  qabsabv  23680  2trllemE  24378  normlem7tALT  25859  hhsssh  26008  shintcli  26070  chintcli  26072  omlsi  26145  qlaxr3i  26377  lnophm  26761  nmcopex  26771  nmcoplb  26772  nmbdfnlbi  26791  nmcfnex  26795  nmcfnlb  26796  hmopidmch  26895  hmopidmpj  26896  chirred  27137  nn0archi  27658  xrge0iifiso  27742  xrge0iifmhm  27746  xrge0pluscn  27747  rezh  27777  qqh0  27790  qqh1  27791  qqhcn  27797  qqhucn  27798  rerrext  27815  cnrrext  27816  mbfmvolf  28062  subfacval3  28458  erdszelem5  28464  erdszelem8  28467  ghomgrpilem2  28851  filnetlem3  30125  filnetlem4  30126  reheibor  30262  islptre  31484  fourierdlem68  31798  fourierdlem77  31807  fourierdlem80  31810  fouriersw  31855  abcdta  31907  abcdtb  31908  abcdtc  31909  zlmodzxzsubm  32427  zlmodzxzldeplem3  32585  ldepsnlinclem1  32588  ldepsnlinclem2  32589  ldepsnlinc  32591  ene1  32650  empty-surprise  32679  bj-pirp  34081  pirp  37166
  Copyright terms: Public domain W3C validator