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  8367  rdgfun  8387  oeoa  8564  oeoe  8566  ssdomg  8974  ordtypelem4  9481  ordtypelem6  9483  ordtypelem7  9484  r1limg  9731  rankwflemb  9753  r1elssi  9765  infxpenlem  9973  ackbij2  10202  wunom  10680  mulnzcnf  11831  negiso  12170  infrenegsup  12173  hashunlei  14397  hashsslei  14398  cos01bnd  16161  cos1bnd  16162  cos2bnd  16163  sin4lt0  16170  egt2lt3  16181  epos  16182  ene1  16185  divalglem5  16374  bitsf1o  16422  gcdaddmlem  16501  sravsca  21095  zrhpsgnmhm  21500  resubgval  21525  re1r  21529  redvr  21533  refld  21535  rzgrp  21539  txindis  23528  icopnfhmeo  24848  iccpnfcnv  24849  iccpnfhmeo  24850  xrhmeo  24851  cnheiborlem  24860  recvs  25053  qcvs  25054  rrxcph  25299  volf  25437  i1f1  25598  itg11  25599  dvsin  25893  taylthlem2  26289  taylthlem2OLD  26290  reefgim  26367  pilem3  26370  pigt2lt4  26371  pire  26373  pipos  26375  sinhalfpi  26384  tan4thpi  26430  tan4thpiOLD  26431  sincos3rdpi  26433  pigt3  26434  circgrp  26468  circsubm  26469  1cubrlem  26758  1cubr  26759  jensenlem2  26905  amgmlem  26907  emcllem6  26918  emcllem7  26919  harmonicbnd3  26925  ppiublem1  27120  chtub  27130  bposlem7  27208  lgsdir2lem4  27246  lgsdir2lem5  27247  chebbnd1  27390  mulog2sumlem2  27453  pntpbnd1a  27503  pntpbnd2  27505  pntlemb  27515  pntlemk  27524  qrng0  27539  qrng1  27540  qrngneg  27541  qrngdiv  27542  qabsabv  27547  ex-sqrt  30390  normlem7tALT  31055  hhsssh  31205  shintcli  31265  chintcli  31267  omlsi  31340  qlaxr3i  31572  lnophm  31955  nmcopex  31965  nmcoplb  31966  nmbdfnlbi  31985  nmcfnex  31989  nmcfnlb  31990  hmopidmch  32089  hmopidmpj  32090  chirred  32331  threehalves  32842  qfld  33254  1fldgenq  33279  nn0archi  33325  ccfldextrr  33649  ccfldsrarelvec  33673  constrextdg2  33746  constrext2chnlem  33747  constrcon  33771  2sqr3minply  33777  2sqr3nconstr  33778  cos9thpiminplylem6  33784  cos9thpiminply  33785  cos9thpinconstrlem2  33787  trisecnconstr  33789  xrge0iifiso  33932  xrge0iifmhm  33936  xrge0pluscn  33937  rezh  33966  qqh0  33981  qqh1  33982  qqhcn  33988  qqhucn  33989  rerrext  34006  cnrrext  34007  mbfmvolf  34264  hgt750lem  34649  subfacval3  35183  erdszelem5  35189  erdszelem8  35192  filnetlem3  36375  filnetlem4  36376  bj-genr  36601  bj-genl  36602  bj-genan  36603  bj-rveccmod  37297  reheibor  37840  cossssid  38465  eqvrelcoss3  38616  3lexlogpow5ineq5  42055  aks6d1c7lem1  42175  tan3rdpi  42347  sin2t3rdpi  42348  sin4t3rdpi  42350  asin1half  42352  fourierdlem68  46179  fourierdlem77  46188  fourierdlem80  46191  fouriersw  46236  etransclem23  46262  gsumge0cl  46376  abcdta  46930  abcdtb  46931  abcdtc  46932  nabctnabc  46936  zlmodzxzsubm  48351  zlmodzxzldeplem3  48495  ldepsnlinclem1  48498  ldepsnlinclem2  48499  ldepsnlinc  48501  sepfsepc  48920  prstcleval  49548  prstcocval  49550  setc1onsubc  49595  empty-surprise  49775  amgmwlem  49795  amgmlemALT  49796