Theorem simpli 488

Description: Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.)

Hypothesis

Ref	Expression
simpli.1	⊢ (𝜑 ∧ 𝜓)

Assertion

Ref	Expression
simpli	⊢ 𝜑

Proof of Theorem simpli

Step	Hyp	Ref	Expression
1		simpli.1	. 2 ⊢ (𝜑 ∧ 𝜓)
2		simpl 487	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
3	1, 2	ax-mp 5	1 ⊢ 𝜑

Syntax hints:   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  tfr2b  8384  rdgfun  8404  oeoa  8584  oeoe  8586  ssdomg  8998  ordtypelem4  9484  ordtypelem6  9486  ordtypelem7  9487  r1limg  9744  rankwflemb  9766  r1elssi  9778  infxpenlem  9998  ackbij2  10226  wunom  10706  mulnzcnf  11861  negiso  12196  infrenegsup  12199  hashunlei  14464  hashsslei  14465  cos01bnd  16243  cos1bnd  16244  cos2bnd  16245  sin4lt0  16252  egt2lt3  16263  epos  16264  ene1  16267  divalglem5  16456  bitsf1o  16504  gcdaddmlem  16583  sravsca  21283  zrhpsgnmhm  21715  resubgval  21740  re1r  21744  redvr  21748  refld  21750  rzgrp  21754  txindis  23772  icopnfhmeo  25083  iccpnfcnv  25084  iccpnfhmeo  25085  xrhmeo  25086  cnheiborlem  25094  recvs  25286  qcvs  25287  rrxcph  25532  volf  25669  i1f1  25830  itg11  25831  dvsin  26122  taylthlem2  26518  reefgim  26594  pilem3  26597  pigt2lt4  26598  pire  26600  pipos  26604  sinhalfpi  26614  tan4thpi  26660  tan4thpiOLD  26661  sincos3rdpi  26663  pigt3  26664  circgrp  26698  circsubm  26699  1cubrlem  26987  1cubr  26988  jensenlem2  27133  amgmlem  27135  emcllem6  27146  emcllem7  27147  harmonicbnd3  27153  ppiublem1  27347  chtub  27357  bposlem7  27435  lgsdir2lem4  27473  lgsdir2lem5  27474  chebbnd1  27617  mulog2sumlem2  27680  pntpbnd1a  27730  pntpbnd2  27732  pntlemb  27742  pntlemk  27751  qrng0  27766  qrng1  27767  qrngneg  27768  qrngdiv  27769  qabsabv  27774  ex-sqrt  30786  normlem7tALT  31452  hhsssh  31602  shintcli  31662  chintcli  31664  omlsi  31737  qlaxr3i  31969  lnophm  32352  nmcopex  32362  nmcoplb  32363  nmbdfnlbi  32382  nmcfnex  32386  nmcfnlb  32387  hmopidmch  32486  hmopidmpj  32487  chirred  32728  threehalves  33215  qfld  33599  1fldgenq  33624  nn0archi  33648  ccfldextrr  34017  ccfldsrarelvec  34042  constrextdg2  34120  constrext2chnlem  34121  constrcon  34145  2sqr3minply  34151  2sqr3nconstr  34152  cos9thpiminplylem6  34158  cos9thpiminply  34159  cos9thpinconstrlem2  34161  trisecnconstr  34163  xrge0iifiso  34306  xrge0iifmhm  34310  xrge0pluscn  34311  rezh  34340  qqh0  34355  qqh1  34356  qqhcn  34362  qqhucn  34363  rerrext  34380  cnrrext  34381  mbfmvolf  34637  hgt750lem  35019  r1filimi  35478  r1filim  35479  r1omfi  35480  r1omhf  35481  r1omfv  35485  subfacval3  35662  erdszelem5  35668  erdszelem8  35671  filnetlem3  36872  filnetlem4  36873  bj-genr  37181  bj-genl  37182  bj-genan  37183  bj-rveccmod  37927  reheibor  38471  cossssid  39187  eqvrelcoss3  39332  3lexlogpow5ineq5  42808  aks6d1c7lem1  42928  tan3rdpi  43094  sin2t3rdpi  43095  sin4t3rdpi  43097  asin1half  43099  fourierdlem68  46871  fourierdlem77  46880  fourierdlem80  46883  fouriersw  46928  etransclem23  46954  gsumge0cl  47068  nthrucw  47590  abcdta  47645  abcdtb  47646  abcdtc  47647  nabctnabc  47651  ppivalnn4  48362  zlmodzxzsubm  49122  zlmodzxzldeplem3  49265  ldepsnlinclem1  49268  ldepsnlinclem2  49269  ldepsnlinc  49271  sepfsepc  49689  prstcleval  50316  prstcocval  50318  setc1onsubc  50363  empty-surprise  50543  amgmwlem  50585  amgmlemALT  50586