Theorem simpli 484

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

Syntax hints:   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  exanOLD  1844  pwundif  5345  tfr2b  7884  rdgfun  7904  oeoa  8073  oeoe  8075  ssdomg  8403  ordtypelem4  8831  ordtypelem6  8833  ordtypelem7  8834  r1limg  9046  rankwflemb  9068  r1elssi  9080  infxpenlem  9285  ackbij2  9511  wunom  9988  mulnzcnopr  11134  negiso  11469  infrenegsup  11472  hashunlei  13634  hashsslei  13635  cos01bnd  15372  cos1bnd  15373  cos2bnd  15374  sin4lt0  15381  egt2lt3  15392  epos  15393  ene1  15396  divalglem5  15581  bitsf1o  15627  gcdaddmlem  15705  zrhpsgnmhm  20410  resubgval  20435  re1r  20439  redvr  20443  refld  20445  rzgrp  20449  txindis  21926  icopnfhmeo  23230  iccpnfcnv  23231  iccpnfhmeo  23232  xrhmeo  23233  cnheiborlem  23241  recvs  23433  qcvs  23434  rrxcph  23678  volf  23813  i1f1  23974  itg11  23975  dvsin  24262  taylthlem2  24645  reefgim  24721  pilem3  24724  pigt2lt4  24725  pire  24727  pipos  24729  sinhalfpi  24737  tan4thpi  24783  sincos3rdpi  24785  pigt3  24786  circgrp  24817  circsubm  24818  1cubrlem  25100  1cubr  25101  jensenlem2  25247  amgmlem  25249  emcllem6  25260  emcllem7  25261  harmonicbnd3  25267  ppiublem1  25460  chtub  25470  bposlem7  25548  lgsdir2lem4  25586  lgsdir2lem5  25587  chebbnd1  25730  mulog2sumlem2  25793  pntpbnd1a  25843  pntpbnd2  25845  pntlemb  25855  pntlemk  25864  qrng0  25879  qrng1  25880  qrngneg  25881  qrngdiv  25882  qabsabv  25887  ex-sqrt  27925  normlem7tALT  28587  hhsssh  28737  shintcli  28797  chintcli  28799  omlsi  28872  qlaxr3i  29104  lnophm  29487  nmcopex  29497  nmcoplb  29498  nmbdfnlbi  29517  nmcfnex  29521  nmcfnlb  29522  hmopidmch  29621  hmopidmpj  29622  chirred  29863  threehalves  30275  nn0archi  30570  ccfldextrr  30642  ccfldsrarelvec  30660  xrge0iifiso  30795  xrge0iifmhm  30799  xrge0pluscn  30800  rezh  30829  qqh0  30842  qqh1  30843  qqhcn  30849  qqhucn  30850  rerrext  30867  cnrrext  30868  mbfmvolf  31141  hgt750lem  31539  subfacval3  32044  erdszelem5  32050  erdszelem8  32053  filnetlem3  33337  filnetlem4  33338  bj-genr  33546  bj-genl  33547  bj-genan  33548  reheibor  34649  cossssid  35238  eqvrelcoss3  35384  fourierdlem68  42001  fourierdlem77  42010  fourierdlem80  42013  fouriersw  42058  etransclem23  42084  gsumge0cl  42195  abcdta  42702  abcdtb  42703  abcdtc  42704  nabctnabc  42708  zlmodzxzsubm  43885  zlmodzxzldeplem3  44037  ldepsnlinclem1  44040  ldepsnlinclem2  44041  ldepsnlinc  44043  empty-surprise  44363  amgmwlem  44383  amgmlemALT  44384