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  8335  rdgfun  8355  oeoa  8533  oeoe  8535  ssdomg  8947  ordtypelem4  9436  ordtypelem6  9438  ordtypelem7  9439  r1limg  9695  rankwflemb  9717  r1elssi  9729  infxpenlem  9935  ackbij2  10164  wunom  10643  mulnzcnf  11796  negiso  12136  infrenegsup  12139  hashunlei  14387  hashsslei  14388  cos01bnd  16153  cos1bnd  16154  cos2bnd  16155  sin4lt0  16162  egt2lt3  16173  epos  16174  ene1  16177  divalglem5  16366  bitsf1o  16414  gcdaddmlem  16493  sravsca  21176  zrhpsgnmhm  21564  resubgval  21589  re1r  21593  redvr  21597  refld  21599  rzgrp  21603  txindis  23599  icopnfhmeo  24910  iccpnfcnv  24911  iccpnfhmeo  24912  xrhmeo  24913  cnheiborlem  24921  recvs  25113  qcvs  25114  rrxcph  25359  volf  25496  i1f1  25657  itg11  25658  dvsin  25949  taylthlem2  26339  reefgim  26415  pilem3  26418  pigt2lt4  26419  pire  26421  pipos  26423  sinhalfpi  26432  tan4thpi  26478  tan4thpiOLD  26479  sincos3rdpi  26481  pigt3  26482  circgrp  26516  circsubm  26517  1cubrlem  26805  1cubr  26806  jensenlem2  26951  amgmlem  26953  emcllem6  26964  emcllem7  26965  harmonicbnd3  26971  ppiublem1  27165  chtub  27175  bposlem7  27253  lgsdir2lem4  27291  lgsdir2lem5  27292  chebbnd1  27435  mulog2sumlem2  27498  pntpbnd1a  27548  pntpbnd2  27550  pntlemb  27560  pntlemk  27569  qrng0  27584  qrng1  27585  qrngneg  27586  qrngdiv  27587  qabsabv  27592  ex-sqrt  30524  normlem7tALT  31190  hhsssh  31340  shintcli  31400  chintcli  31402  omlsi  31475  qlaxr3i  31707  lnophm  32090  nmcopex  32100  nmcoplb  32101  nmbdfnlbi  32120  nmcfnex  32124  nmcfnlb  32125  hmopidmch  32224  hmopidmpj  32225  chirred  32466  threehalves  32974  qfld  33358  1fldgenq  33383  nn0archi  33407  ccfldextrr  33790  ccfldsrarelvec  33815  constrextdg2  33893  constrext2chnlem  33894  constrcon  33918  2sqr3minply  33924  2sqr3nconstr  33925  cos9thpiminplylem6  33931  cos9thpiminply  33932  cos9thpinconstrlem2  33934  trisecnconstr  33936  xrge0iifiso  34079  xrge0iifmhm  34083  xrge0pluscn  34084  rezh  34113  qqh0  34128  qqh1  34129  qqhcn  34135  qqhucn  34136  rerrext  34153  cnrrext  34154  mbfmvolf  34410  hgt750lem  34795  r1filimi  35246  r1filim  35247  r1omfi  35248  r1omhf  35249  r1omfv  35254  subfacval3  35371  erdszelem5  35377  erdszelem8  35380  filnetlem3  36562  filnetlem4  36563  bj-genr  36872  bj-genl  36873  bj-genan  36874  bj-rveccmod  37616  reheibor  38160  cossssid  38878  eqvrelcoss3  39023  3lexlogpow5ineq5  42499  aks6d1c7lem1  42619  tan3rdpi  42784  sin2t3rdpi  42785  sin4t3rdpi  42787  asin1half  42789  fourierdlem68  46602  fourierdlem77  46611  fourierdlem80  46614  fouriersw  46659  etransclem23  46685  gsumge0cl  46799  nthrucw  47316  abcdta  47373  abcdtb  47374  abcdtc  47375  nabctnabc  47379  ppivalnn4  48090  zlmodzxzsubm  48835  zlmodzxzldeplem3  48978  ldepsnlinclem1  48981  ldepsnlinclem2  48982  ldepsnlinc  48984  sepfsepc  49403  prstcleval  50030  prstcocval  50032  setc1onsubc  50077  empty-surprise  50257  amgmwlem  50277  amgmlemALT  50278