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

Theorem simpli 444
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 443 . 2  |-  ( (
ph  /\  ps )  ->  ph )
31, 2ax-mp 8 1  |-  ph
Colors of variables: wff set class
Syntax hints:    /\ wa 358
This theorem is referenced by:  pwundif  4300  tfr2b  6412  rdgfun  6429  oeoa  6595  oeoe  6597  ssdomg  6907  ordtypelem4  7236  ordtypelem6  7238  ordtypelem7  7239  r1limg  7443  rankwflemb  7465  r1elssi  7477  infxpenlem  7641  ackbij2  7869  wunom  8342  mulnzcnopr  9414  negiso  9730  infmsup  9732  hashunlei  11377  hashsslei  11378  cos01bnd  12466  cos1bnd  12467  cos2bnd  12468  sin4lt0  12475  egt2lt3  12484  epos  12485  divalglem5  12596  bitsf1o  12636  gcdaddmlem  12707  strlemor1  13235  txindis  17328  icopnfhmeo  18441  iccpnfcnv  18442  iccpnfhmeo  18443  xrhmeo  18444  cnheiborlem  18452  volf  18888  i1f1  19045  itg11  19046  dvsin  19329  taylthlem2  19753  reefgim  19826  pilem3  19829  pigt2lt4  19830  pire  19832  pipos  19833  sinhalfpi  19836  tan4thpi  19882  sincos3rdpi  19884  1cubrlem  20137  1cubr  20138  jensenlem2  20282  amgmlem  20284  emcllem6  20294  emcllem7  20295  emgt0  20300  harmonicbnd3  20301  ppiublem1  20441  chtub  20451  bposlem7  20529  lgsdir2lem4  20565  lgsdir2lem5  20566  chebbnd1  20621  mulog2sumlem2  20684  pntpbnd1a  20734  pntpbnd2  20736  pntlemb  20746  pntlemk  20755  qrng0  20770  qrng1  20771  qrngneg  20772  qrngdiv  20773  qabsabv  20778  normlem7tALT  21698  hhsssh  21846  shintcli  21908  chintcli  21910  omlsi  21983  qlaxr3i  22215  lnophm  22599  nmcopex  22609  nmcoplb  22610  nmbdfnlbi  22629  nmcfnex  22633  nmcfnlb  22634  hmopidmch  22733  hmopidmpj  22734  chirred  22975  pwundif2  23186  xrge0iifiso  23317  xrge0iifmhm  23321  xrge0pluscn  23322  mbfmvolf  23571  subfacval3  23720  erdszelem5  23726  erdszelem8  23729  ghomgrpilem2  23993  cntrset  25602  pvp  26048  filnetlem3  26329  filnetlem4  26330  reheibor  26563
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator