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  8315  rdgfun  8335  oeoa  8512  oeoe  8514  ssdomg  8922  ordtypelem4  9407  ordtypelem6  9409  ordtypelem7  9410  r1limg  9664  rankwflemb  9686  r1elssi  9698  infxpenlem  9904  ackbij2  10133  wunom  10611  mulnzcnf  11763  negiso  12102  infrenegsup  12105  hashunlei  14332  hashsslei  14333  cos01bnd  16095  cos1bnd  16096  cos2bnd  16097  sin4lt0  16104  egt2lt3  16115  epos  16116  ene1  16119  divalglem5  16308  bitsf1o  16356  gcdaddmlem  16435  sravsca  21116  zrhpsgnmhm  21522  resubgval  21547  re1r  21551  redvr  21555  refld  21557  rzgrp  21561  txindis  23550  icopnfhmeo  24869  iccpnfcnv  24870  iccpnfhmeo  24871  xrhmeo  24872  cnheiborlem  24881  recvs  25074  qcvs  25075  rrxcph  25320  volf  25458  i1f1  25619  itg11  25620  dvsin  25914  taylthlem2  26310  taylthlem2OLD  26311  reefgim  26388  pilem3  26391  pigt2lt4  26392  pire  26394  pipos  26396  sinhalfpi  26405  tan4thpi  26451  tan4thpiOLD  26452  sincos3rdpi  26454  pigt3  26455  circgrp  26489  circsubm  26490  1cubrlem  26779  1cubr  26780  jensenlem2  26926  amgmlem  26928  emcllem6  26939  emcllem7  26940  harmonicbnd3  26946  ppiublem1  27141  chtub  27151  bposlem7  27229  lgsdir2lem4  27267  lgsdir2lem5  27268  chebbnd1  27411  mulog2sumlem2  27474  pntpbnd1a  27524  pntpbnd2  27526  pntlemb  27536  pntlemk  27545  qrng0  27560  qrng1  27561  qrngneg  27562  qrngdiv  27563  qabsabv  27568  ex-sqrt  30432  normlem7tALT  31097  hhsssh  31247  shintcli  31307  chintcli  31309  omlsi  31382  qlaxr3i  31614  lnophm  31997  nmcopex  32007  nmcoplb  32008  nmbdfnlbi  32027  nmcfnex  32031  nmcfnlb  32032  hmopidmch  32131  hmopidmpj  32132  chirred  32373  threehalves  32893  qfld  33261  1fldgenq  33286  nn0archi  33310  ccfldextrr  33657  ccfldsrarelvec  33682  constrextdg2  33760  constrext2chnlem  33761  constrcon  33785  2sqr3minply  33791  2sqr3nconstr  33792  cos9thpiminplylem6  33798  cos9thpiminply  33799  cos9thpinconstrlem2  33801  trisecnconstr  33803  xrge0iifiso  33946  xrge0iifmhm  33950  xrge0pluscn  33951  rezh  33980  qqh0  33995  qqh1  33996  qqhcn  34002  qqhucn  34003  rerrext  34020  cnrrext  34021  mbfmvolf  34277  hgt750lem  34662  r1filimi  35112  r1filim  35113  r1omfi  35114  r1omhf  35115  r1omfv  35119  subfacval3  35231  erdszelem5  35237  erdszelem8  35240  filnetlem3  36420  filnetlem4  36421  bj-genr  36646  bj-genl  36647  bj-genan  36648  bj-rveccmod  37342  reheibor  37885  cossssid  38510  eqvrelcoss3  38661  3lexlogpow5ineq5  42099  aks6d1c7lem1  42219  tan3rdpi  42391  sin2t3rdpi  42392  sin4t3rdpi  42394  asin1half  42396  fourierdlem68  46218  fourierdlem77  46227  fourierdlem80  46230  fouriersw  46275  etransclem23  46301  gsumge0cl  46415  abcdta  46962  abcdtb  46963  abcdtc  46964  nabctnabc  46968  zlmodzxzsubm  48396  zlmodzxzldeplem3  48540  ldepsnlinclem1  48543  ldepsnlinclem2  48544  ldepsnlinc  48546  sepfsepc  48965  prstcleval  49593  prstcocval  49595  setc1onsubc  49640  empty-surprise  49820  amgmwlem  49840  amgmlemALT  49841