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

Theorem simpli 445
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 444 . 2  |-  ( (
ph  /\  ps )  ->  ph )
31, 2ax-mp 8 1  |-  ph
Colors of variables: wff set class
Syntax hints:    /\ wa 359
This theorem is referenced by:  pwundif  4450  tfr2b  6616  rdgfun  6633  oeoa  6799  oeoe  6801  ssdomg  7112  ordtypelem4  7446  ordtypelem6  7448  ordtypelem7  7449  r1limg  7653  rankwflemb  7675  r1elssi  7687  infxpenlem  7851  ackbij2  8079  wunom  8551  mulnzcnopr  9624  negiso  9940  infmsup  9942  hashunlei  11639  hashsslei  11640  cos01bnd  12742  cos1bnd  12743  cos2bnd  12744  sin4lt0  12751  egt2lt3  12760  epos  12761  divalglem5  12872  bitsf1o  12912  gcdaddmlem  12983  strlemor1  13511  txindis  17619  icopnfhmeo  18921  iccpnfcnv  18922  iccpnfhmeo  18923  xrhmeo  18924  cnheiborlem  18932  volf  19378  i1f1  19535  itg11  19536  dvsin  19819  taylthlem2  20243  reefgim  20319  pilem3  20322  pigt2lt4  20323  pire  20325  pipos  20326  sinhalfpi  20329  tan4thpi  20375  sincos3rdpi  20377  1cubrlem  20634  1cubr  20635  jensenlem2  20779  amgmlem  20781  emcllem6  20792  emcllem7  20793  emgt0  20798  harmonicbnd3  20799  ppiublem1  20939  chtub  20949  bposlem7  21027  lgsdir2lem4  21063  lgsdir2lem5  21064  chebbnd1  21119  mulog2sumlem2  21182  pntpbnd1a  21232  pntpbnd2  21234  pntlemb  21244  pntlemk  21253  qrng0  21268  qrng1  21269  qrngneg  21270  qrngdiv  21271  qabsabv  21276  2trllemE  21506  normlem7tALT  22574  hhsssh  22722  shintcli  22784  chintcli  22786  omlsi  22859  qlaxr3i  23091  lnophm  23475  nmcopex  23485  nmcoplb  23486  nmbdfnlbi  23505  nmcfnex  23509  nmcfnlb  23510  hmopidmch  23609  hmopidmpj  23610  chirred  23851  re1r  24227  redvr  24230  refld  24232  xrge0iifiso  24274  xrge0iifmhm  24278  xrge0pluscn  24279  rezh  24308  qqh0  24321  qqh1  24322  qqhcn  24328  qqhucn  24329  rrhre  24340  mbfmvolf  24569  sitgclcn  24611  sitmcl  24616  subfacval3  24828  erdszelem5  24834  erdszelem8  24837  ghomgrpilem2  25050  filnetlem3  26299  filnetlem4  26300  reheibor  26438  abcdta  27757  abcdtb  27758  abcdtc  27759  ene1  28245
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 178  df-an 361
  Copyright terms: Public domain W3C validator