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  8364  rdgfun  8384  oeoa  8561  oeoe  8563  ssdomg  8971  ordtypelem4  9474  ordtypelem6  9476  ordtypelem7  9477  r1limg  9724  rankwflemb  9746  r1elssi  9758  infxpenlem  9966  ackbij2  10195  wunom  10673  mulnzcnf  11824  negiso  12163  infrenegsup  12166  hashunlei  14390  hashsslei  14391  cos01bnd  16154  cos1bnd  16155  cos2bnd  16156  sin4lt0  16163  egt2lt3  16174  epos  16175  ene1  16178  divalglem5  16367  bitsf1o  16415  gcdaddmlem  16494  sravsca  21088  zrhpsgnmhm  21493  resubgval  21518  re1r  21522  redvr  21526  refld  21528  rzgrp  21532  txindis  23521  icopnfhmeo  24841  iccpnfcnv  24842  iccpnfhmeo  24843  xrhmeo  24844  cnheiborlem  24853  recvs  25046  qcvs  25047  rrxcph  25292  volf  25430  i1f1  25591  itg11  25592  dvsin  25886  taylthlem2  26282  taylthlem2OLD  26283  reefgim  26360  pilem3  26363  pigt2lt4  26364  pire  26366  pipos  26368  sinhalfpi  26377  tan4thpi  26423  tan4thpiOLD  26424  sincos3rdpi  26426  pigt3  26427  circgrp  26461  circsubm  26462  1cubrlem  26751  1cubr  26752  jensenlem2  26898  amgmlem  26900  emcllem6  26911  emcllem7  26912  harmonicbnd3  26918  ppiublem1  27113  chtub  27123  bposlem7  27201  lgsdir2lem4  27239  lgsdir2lem5  27240  chebbnd1  27383  mulog2sumlem2  27446  pntpbnd1a  27496  pntpbnd2  27498  pntlemb  27508  pntlemk  27517  qrng0  27532  qrng1  27533  qrngneg  27534  qrngdiv  27535  qabsabv  27540  ex-sqrt  30383  normlem7tALT  31048  hhsssh  31198  shintcli  31258  chintcli  31260  omlsi  31333  qlaxr3i  31565  lnophm  31948  nmcopex  31958  nmcoplb  31959  nmbdfnlbi  31978  nmcfnex  31982  nmcfnlb  31983  hmopidmch  32082  hmopidmpj  32083  chirred  32324  threehalves  32835  qfld  33247  1fldgenq  33272  nn0archi  33318  ccfldextrr  33642  ccfldsrarelvec  33666  constrextdg2  33739  constrext2chnlem  33740  constrcon  33764  2sqr3minply  33770  2sqr3nconstr  33771  cos9thpiminplylem6  33777  cos9thpiminply  33778  cos9thpinconstrlem2  33780  trisecnconstr  33782  xrge0iifiso  33925  xrge0iifmhm  33929  xrge0pluscn  33930  rezh  33959  qqh0  33974  qqh1  33975  qqhcn  33981  qqhucn  33982  rerrext  33999  cnrrext  34000  mbfmvolf  34257  hgt750lem  34642  subfacval3  35176  erdszelem5  35182  erdszelem8  35185  filnetlem3  36368  filnetlem4  36369  bj-genr  36594  bj-genl  36595  bj-genan  36596  bj-rveccmod  37290  reheibor  37833  cossssid  38458  eqvrelcoss3  38609  3lexlogpow5ineq5  42048  aks6d1c7lem1  42168  tan3rdpi  42340  sin2t3rdpi  42341  sin4t3rdpi  42343  asin1half  42345  fourierdlem68  46172  fourierdlem77  46181  fourierdlem80  46184  fouriersw  46229  etransclem23  46255  gsumge0cl  46369  abcdta  46926  abcdtb  46927  abcdtc  46928  nabctnabc  46932  zlmodzxzsubm  48347  zlmodzxzldeplem3  48491  ldepsnlinclem1  48494  ldepsnlinclem2  48495  ldepsnlinc  48497  sepfsepc  48916  prstcleval  49544  prstcocval  49546  setc1onsubc  49591  empty-surprise  49771  amgmwlem  49791  amgmlemALT  49792