Theorem simpli 489

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

This proof depends on syntax axioms:   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  tfr2b  8435  rdgfun  8455  oeoa  8637  oeoe  8639  ssdomg  9058  ordtypelem4  9545  ordtypelem6  9547  ordtypelem7  9548  infxpenlem  10122  mulnzcnf  11992  negiso  12327  infrenegsup  12330  hashunlei  14600  hashsslei  14601  cos01bnd  16386  cos1bnd  16387  cos2bnd  16388  sin4lt0  16395  egt2lt3  16406  epos  16407  ene1  16410  divalglem5  16599  bitsf1o  16647  gcdaddmlem  16728  sravsca  21489  zrhpsgnmhm  21923  resubgval  21948  re1r  21952  redvr  21956  refld  21958  rzgrp  21962  txindis  23986  icopnfhmeo  25297  iccpnfcnv  25298  iccpnfhmeo  25299  xrhmeo  25300  cnheiborlem  25308  recvs  25500  qcvs  25501  rrxcph  25746  volf  25883  i1f1  26044  itg11  26045  dvsin  26335  taylthlem2  26734  reefgim  26810  pilem3  26813  pigt2lt4  26814  pire  26816  pipos  26820  sinhalfpi  26830  tan4thpi  26876  sincos3rdpi  26878  pigt3  26879  circgrp  26913  circsubm  26914  1cubrlem  27202  1cubr  27203  jensenlem2  27348  amgmlem  27350  emcllem6  27361  emcllem7  27362  harmonicbnd3  27368  ppiublem1  27562  chtub  27572  bposlem7  27650  lgsdir2lem4  27688  lgsdir2lem5  27689  chebbnd1  27832  mulog2sumlem2  27895  pntpbnd1a  27945  pntpbnd2  27947  pntlemb  27957  pntlemk  27966  qrng0  27981  qrng1  27982  qrngneg  27983  qrngdiv  27984  qabsabv  27989  ex-sqrt  31088  normlem7tALT  31754  hhsssh  31904  shintcli  31964  chintcli  31966  omlsi  32039  qlaxr3i  32271  lnophm  32654  nmcopex  32664  nmcoplb  32665  nmbdfnlbi  32684  nmcfnex  32688  nmcfnlb  32689  hmopidmch  32788  hmopidmpj  32789  chirred  33030  threehalves  33554  qfld  33943  1fldgenq  33968  nn0archi  33992  ccfldextrr  34361  ccfldsrarelvec  34386  constrextdg2  34464  constrext2chnlem  34465  constrcon  34489  2sqr3minply  34495  2sqr3nconstr  34496  cos9thpiminplylem6  34502  cos9thpiminply  34503  cos9thpinconstrlem2  34505  trisecnconstr  34507  xrge0iifiso  34650  xrge0iifmhm  34654  xrge0pluscn  34655  rezh  34684  qqh0  34699  qqh1  34700  qqhcn  34706  qqhucn  34707  rerrext  34724  cnrrext  34725  mbfmvolf  34981  hgt750lem  35363  subfacval3  36134  erdszelem5  36140  erdszelem8  36143  filnetlem3  37359  filnetlem4  37360  bj-genr  37668  bj-genl  37669  bj-genan  37670  bj-rveccmod  38428  reheibor  38976  cossssid  39692  eqvrelcoss3  39837  3lexlogpow5ineq5  43313  aks6d1c7lem1  43433  tan3rdpi  43607  sin2t3rdpi  43608  sin4t3rdpi  43610  asin1half  43612  fourierdlem68  47399  fourierdlem77  47408  fourierdlem80  47411  fouriersw  47456  etransclem23  47482  gsumge0cl  47596  numtowerdt  48131  abcdta  48210  abcdtb  48211  abcdtc  48212  nabctnabc  48216  ppivalnn4  48927  zlmodzxzsubm  49686  zlmodzxzldeplem3  49829  ldepsnlinclem1  49832  ldepsnlinclem2  49833  ldepsnlinc  49835  sepfsepc  50257  prstcleval  50908  prstcocval  50910  setc1onsubc  50955  par2cat  50983  parswapfunc  50993  par2diag  50995  fuconuniqlem  50996  fuconuniqvalslem  50998  empty-surprise  51190  veroquadmodzerod  51296  veroquadnolindfd  51297  veroquaddetzerod  51298  amgmwlem  51299  amgmlemALT  51300