Theorem simpli 483

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 482	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
3	1, 2	ax-mp 5	1 ⊢ 𝜑

Syntax hints:   ∧ wa 395

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 206  df-an 396

This theorem is referenced by:  pwundifOLD  5477  tfr2b  8198  rdgfun  8218  oeoa  8390  oeoe  8392  ssdomg  8741  ordtypelem4  9210  ordtypelem6  9212  ordtypelem7  9213  r1limg  9460  rankwflemb  9482  r1elssi  9494  infxpenlem  9700  ackbij2  9930  wunom  10407  mulnzcnopr  11551  negiso  11885  infrenegsup  11888  hashunlei  14068  hashsslei  14069  cos01bnd  15823  cos1bnd  15824  cos2bnd  15825  sin4lt0  15832  egt2lt3  15843  epos  15844  ene1  15847  divalglem5  16034  bitsf1o  16080  gcdaddmlem  16159  zrhpsgnmhm  20701  resubgval  20726  re1r  20730  redvr  20734  refld  20736  rzgrp  20740  txindis  22693  icopnfhmeo  24012  iccpnfcnv  24013  iccpnfhmeo  24014  xrhmeo  24015  cnheiborlem  24023  recvs  24215  qcvs  24216  rrxcph  24461  volf  24598  i1f1  24759  itg11  24760  dvsin  25051  taylthlem2  25438  reefgim  25514  pilem3  25517  pigt2lt4  25518  pire  25520  pipos  25522  sinhalfpi  25530  tan4thpi  25576  sincos3rdpi  25578  pigt3  25579  circgrp  25613  circsubm  25614  1cubrlem  25896  1cubr  25897  jensenlem2  26042  amgmlem  26044  emcllem6  26055  emcllem7  26056  harmonicbnd3  26062  ppiublem1  26255  chtub  26265  bposlem7  26343  lgsdir2lem4  26381  lgsdir2lem5  26382  chebbnd1  26525  mulog2sumlem2  26588  pntpbnd1a  26638  pntpbnd2  26640  pntlemb  26650  pntlemk  26659  qrng0  26674  qrng1  26675  qrngneg  26676  qrngdiv  26677  qabsabv  26682  ex-sqrt  28719  normlem7tALT  29382  hhsssh  29532  shintcli  29592  chintcli  29594  omlsi  29667  qlaxr3i  29899  lnophm  30282  nmcopex  30292  nmcoplb  30293  nmbdfnlbi  30312  nmcfnex  30316  nmcfnlb  30317  hmopidmch  30416  hmopidmpj  30417  chirred  30658  threehalves  31091  nn0archi  31449  ccfldextrr  31625  ccfldsrarelvec  31643  xrge0iifiso  31787  xrge0iifmhm  31791  xrge0pluscn  31792  rezh  31821  qqh0  31834  qqh1  31835  qqhcn  31841  qqhucn  31842  rerrext  31859  cnrrext  31860  mbfmvolf  32133  hgt750lem  32531  subfacval3  33051  erdszelem5  33057  erdszelem8  33060  filnetlem3  34496  filnetlem4  34497  bj-genr  34715  bj-genl  34716  bj-genan  34717  bj-rveccmod  35400  reheibor  35924  cossssid  36512  eqvrelcoss3  36658  3lexlogpow5ineq5  39996  fourierdlem68  43605  fourierdlem77  43614  fourierdlem80  43617  fouriersw  43662  etransclem23  43688  gsumge0cl  43799  abcdta  44307  abcdtb  44308  abcdtc  44309  nabctnabc  44313  zlmodzxzsubm  45583  zlmodzxzldeplem3  45731  ldepsnlinclem1  45734  ldepsnlinclem2  45735  ldepsnlinc  45737  sepfsepc  46109  empty-surprise  46372  amgmwlem  46392  amgmlemALT  46393