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

This theorem is referenced by:  tfr2b  8436  rdgfun  8456  oeoa  8635  oeoe  8637  ssdomg  9040  ordtypelem4  9561  ordtypelem6  9563  ordtypelem7  9564  r1limg  9811  rankwflemb  9833  r1elssi  9845  infxpenlem  10053  ackbij2  10282  wunom  10760  mulnzcnf  11909  negiso  12248  infrenegsup  12251  hashunlei  14464  hashsslei  14465  cos01bnd  16222  cos1bnd  16223  cos2bnd  16224  sin4lt0  16231  egt2lt3  16242  epos  16243  ene1  16246  divalglem5  16434  bitsf1o  16482  gcdaddmlem  16561  sravsca  21185  zrhpsgnmhm  21602  resubgval  21627  re1r  21631  redvr  21635  refld  21637  rzgrp  21641  txindis  23642  icopnfhmeo  24974  iccpnfcnv  24975  iccpnfhmeo  24976  xrhmeo  24977  cnheiborlem  24986  recvs  25179  recvsOLD  25180  qcvs  25181  rrxcph  25426  volf  25564  i1f1  25725  itg11  25726  dvsin  26020  taylthlem2  26416  taylthlem2OLD  26417  reefgim  26494  pilem3  26497  pigt2lt4  26498  pire  26500  pipos  26502  sinhalfpi  26510  tan4thpi  26556  tan4thpiOLD  26557  sincos3rdpi  26559  pigt3  26560  circgrp  26594  circsubm  26595  1cubrlem  26884  1cubr  26885  jensenlem2  27031  amgmlem  27033  emcllem6  27044  emcllem7  27045  harmonicbnd3  27051  ppiublem1  27246  chtub  27256  bposlem7  27334  lgsdir2lem4  27372  lgsdir2lem5  27373  chebbnd1  27516  mulog2sumlem2  27579  pntpbnd1a  27629  pntpbnd2  27631  pntlemb  27641  pntlemk  27650  qrng0  27665  qrng1  27666  qrngneg  27667  qrngdiv  27668  qabsabv  27673  ex-sqrt  30473  normlem7tALT  31138  hhsssh  31288  shintcli  31348  chintcli  31350  omlsi  31423  qlaxr3i  31655  lnophm  32038  nmcopex  32048  nmcoplb  32049  nmbdfnlbi  32068  nmcfnex  32072  nmcfnlb  32073  hmopidmch  32172  hmopidmpj  32173  chirred  32414  threehalves  32897  qfld  33300  1fldgenq  33324  nn0archi  33375  ccfldextrr  33699  ccfldsrarelvec  33721  constrextdg2  33790  2sqr3minply  33791  xrge0iifiso  33934  xrge0iifmhm  33938  xrge0pluscn  33939  rezh  33970  qqh0  33985  qqh1  33986  qqhcn  33992  qqhucn  33993  rerrext  34010  cnrrext  34011  mbfmvolf  34268  hgt750lem  34666  subfacval3  35194  erdszelem5  35200  erdszelem8  35203  filnetlem3  36381  filnetlem4  36382  bj-genr  36607  bj-genl  36608  bj-genan  36609  bj-rveccmod  37303  reheibor  37846  cossssid  38468  eqvrelcoss3  38619  3lexlogpow5ineq5  42061  aks6d1c7lem1  42181  tan3rdpi  42386  asin1half  42387  fourierdlem68  46189  fourierdlem77  46198  fourierdlem80  46201  fouriersw  46246  etransclem23  46272  gsumge0cl  46386  abcdta  46937  abcdtb  46938  abcdtc  46939  nabctnabc  46943  zlmodzxzsubm  48275  zlmodzxzldeplem3  48419  ldepsnlinclem1  48422  ldepsnlinclem2  48423  ldepsnlinc  48425  sepfsepc  48825  prstcleval  49157  prstcocval  49160  empty-surprise  49301  amgmwlem  49321  amgmlemALT  49322