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:  tfr2b  8325  rdgfun  8345  oeoa  8523  oeoe  8525  ssdomg  8937  ordtypelem4  9426  ordtypelem6  9428  ordtypelem7  9429  r1limg  9686  rankwflemb  9708  r1elssi  9720  infxpenlem  9926  ackbij2  10155  wunom  10634  mulnzcnf  11787  negiso  12127  infrenegsup  12130  hashunlei  14378  hashsslei  14379  cos01bnd  16144  cos1bnd  16145  cos2bnd  16146  sin4lt0  16153  egt2lt3  16164  epos  16165  ene1  16168  divalglem5  16357  bitsf1o  16405  gcdaddmlem  16484  sravsca  21171  zrhpsgnmhm  21559  resubgval  21584  re1r  21588  redvr  21592  refld  21594  rzgrp  21598  txindis  23617  icopnfhmeo  24928  iccpnfcnv  24929  iccpnfhmeo  24930  xrhmeo  24931  cnheiborlem  24939  recvs  25131  qcvs  25132  rrxcph  25377  volf  25514  i1f1  25675  itg11  25676  dvsin  25967  taylthlem2  26357  reefgim  26433  pilem3  26436  pigt2lt4  26437  pire  26439  pipos  26441  sinhalfpi  26450  tan4thpi  26496  tan4thpiOLD  26497  sincos3rdpi  26499  pigt3  26500  circgrp  26534  circsubm  26535  1cubrlem  26823  1cubr  26824  jensenlem2  26969  amgmlem  26971  emcllem6  26982  emcllem7  26983  harmonicbnd3  26989  ppiublem1  27183  chtub  27193  bposlem7  27271  lgsdir2lem4  27309  lgsdir2lem5  27310  chebbnd1  27453  mulog2sumlem2  27516  pntpbnd1a  27566  pntpbnd2  27568  pntlemb  27578  pntlemk  27587  qrng0  27602  qrng1  27603  qrngneg  27604  qrngdiv  27605  qabsabv  27610  ex-sqrt  30542  normlem7tALT  31208  hhsssh  31358  shintcli  31418  chintcli  31420  omlsi  31493  qlaxr3i  31725  lnophm  32108  nmcopex  32118  nmcoplb  32119  nmbdfnlbi  32138  nmcfnex  32142  nmcfnlb  32143  hmopidmch  32242  hmopidmpj  32243  chirred  32484  threehalves  32993  qfld  33381  1fldgenq  33406  nn0archi  33430  ccfldextrr  33830  ccfldsrarelvec  33855  constrextdg2  33933  constrext2chnlem  33934  constrcon  33958  2sqr3minply  33964  2sqr3nconstr  33965  cos9thpiminplylem6  33971  cos9thpiminply  33972  cos9thpinconstrlem2  33974  trisecnconstr  33976  xrge0iifiso  34119  xrge0iifmhm  34123  xrge0pluscn  34124  rezh  34153  qqh0  34168  qqh1  34169  qqhcn  34175  qqhucn  34176  rerrext  34193  cnrrext  34194  mbfmvolf  34450  hgt750lem  34835  r1filimi  35284  r1filim  35285  r1omfi  35286  r1omhf  35287  r1omfv  35291  subfacval3  35417  erdszelem5  35423  erdszelem8  35426  filnetlem3  36608  filnetlem4  36609  bj-genr  36918  bj-genl  36919  bj-genan  36920  bj-rveccmod  37662  reheibor  38206  cossssid  38924  eqvrelcoss3  39069  3lexlogpow5ineq5  42545  aks6d1c7lem1  42665  tan3rdpi  42829  sin2t3rdpi  42830  sin4t3rdpi  42832  asin1half  42834  fourierdlem68  46617  fourierdlem77  46626  fourierdlem80  46629  fouriersw  46674  etransclem23  46700  gsumge0cl  46814  nthrucw  47331  abcdta  47388  abcdtb  47389  abcdtc  47390  nabctnabc  47394  ppivalnn4  48105  zlmodzxzsubm  48850  zlmodzxzldeplem3  48993  ldepsnlinclem1  48996  ldepsnlinclem2  48997  ldepsnlinc  48999  sepfsepc  49418  prstcleval  50045  prstcocval  50047  setc1onsubc  50092  empty-surprise  50272  amgmwlem  50292  amgmlemALT  50293