MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simpli Structured version   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  4490  tfr2b  6657  rdgfun  6674  oeoa  6840  oeoe  6842  ssdomg  7153  ordtypelem4  7490  ordtypelem6  7492  ordtypelem7  7493  r1limg  7697  rankwflemb  7719  r1elssi  7731  infxpenlem  7895  ackbij2  8123  wunom  8595  mulnzcnopr  9668  negiso  9984  infmsup  9986  hashunlei  11684  hashsslei  11685  cos01bnd  12787  cos1bnd  12788  cos2bnd  12789  sin4lt0  12796  egt2lt3  12805  epos  12806  divalglem5  12917  bitsf1o  12957  gcdaddmlem  13028  strlemor1  13556  txindis  17666  icopnfhmeo  18968  iccpnfcnv  18969  iccpnfhmeo  18970  xrhmeo  18971  cnheiborlem  18979  volf  19425  i1f1  19582  itg11  19583  dvsin  19866  taylthlem2  20290  reefgim  20366  pilem3  20369  pigt2lt4  20370  pire  20372  pipos  20373  sinhalfpi  20376  tan4thpi  20422  sincos3rdpi  20424  1cubrlem  20681  1cubr  20682  jensenlem2  20826  amgmlem  20828  emcllem6  20839  emcllem7  20840  emgt0  20845  harmonicbnd3  20846  ppiublem1  20986  chtub  20996  bposlem7  21074  lgsdir2lem4  21110  lgsdir2lem5  21111  chebbnd1  21166  mulog2sumlem2  21229  pntpbnd1a  21279  pntpbnd2  21281  pntlemb  21291  pntlemk  21300  qrng0  21315  qrng1  21316  qrngneg  21317  qrngdiv  21318  qabsabv  21323  2trllemE  21553  normlem7tALT  22621  hhsssh  22769  shintcli  22831  chintcli  22833  omlsi  22906  qlaxr3i  23138  lnophm  23522  nmcopex  23532  nmcoplb  23533  nmbdfnlbi  23552  nmcfnex  23556  nmcfnlb  23557  hmopidmch  23656  hmopidmpj  23657  chirred  23898  re1r  24274  redvr  24277  refld  24279  xrge0iifiso  24321  xrge0iifmhm  24325  xrge0pluscn  24326  rezh  24355  qqh0  24368  qqh1  24369  qqhcn  24375  qqhucn  24376  rrhre  24387  mbfmvolf  24616  sitgclcn  24658  sitmcl  24663  subfacval3  24875  erdszelem5  24881  erdszelem8  24884  ghomgrpilem2  25097  filnetlem3  26409  filnetlem4  26410  reheibor  26548  abcdta  27866  abcdtb  27867  abcdtc  27868  ene1  28531
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