Theorem simpli 488

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

Syntax hints:   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  tfr2b  8371  rdgfun  8391  oeoa  8571  oeoe  8573  ssdomg  8985  ordtypelem4  9471  ordtypelem6  9473  ordtypelem7  9474  r1limg  9731  rankwflemb  9753  r1elssi  9765  infxpenlem  9985  ackbij2  10213  wunom  10693  mulnzcnf  11848  negiso  12186  infrenegsup  12189  hashunlei  14452  hashsslei  14453  cos01bnd  16232  cos1bnd  16233  cos2bnd  16234  sin4lt0  16241  egt2lt3  16252  epos  16253  ene1  16256  divalglem5  16445  bitsf1o  16493  gcdaddmlem  16572  sravsca  21271  zrhpsgnmhm  21694  resubgval  21719  re1r  21723  redvr  21727  refld  21729  rzgrp  21733  txindis  23752  icopnfhmeo  25063  iccpnfcnv  25064  iccpnfhmeo  25065  xrhmeo  25066  cnheiborlem  25074  recvs  25266  qcvs  25267  rrxcph  25512  volf  25649  i1f1  25810  itg11  25811  dvsin  26102  taylthlem2  26495  reefgim  26571  pilem3  26574  pigt2lt4  26575  pire  26577  pipos  26581  sinhalfpi  26591  tan4thpi  26637  tan4thpiOLD  26638  sincos3rdpi  26640  pigt3  26641  circgrp  26675  circsubm  26676  1cubrlem  26964  1cubr  26965  jensenlem2  27110  amgmlem  27112  emcllem6  27123  emcllem7  27124  harmonicbnd3  27130  ppiublem1  27324  chtub  27334  bposlem7  27412  lgsdir2lem4  27450  lgsdir2lem5  27451  chebbnd1  27594  mulog2sumlem2  27657  pntpbnd1a  27707  pntpbnd2  27709  pntlemb  27719  pntlemk  27728  qrng0  27743  qrng1  27744  qrngneg  27745  qrngdiv  27746  qabsabv  27751  ex-sqrt  30714  normlem7tALT  31380  hhsssh  31530  shintcli  31590  chintcli  31592  omlsi  31665  qlaxr3i  31897  lnophm  32280  nmcopex  32290  nmcoplb  32291  nmbdfnlbi  32310  nmcfnex  32314  nmcfnlb  32315  hmopidmch  32414  hmopidmpj  32415  chirred  32656  threehalves  33147  qfld  33533  1fldgenq  33558  nn0archi  33582  ccfldextrr  33953  ccfldsrarelvec  33978  constrextdg2  34056  constrext2chnlem  34057  constrcon  34081  2sqr3minply  34087  2sqr3nconstr  34088  cos9thpiminplylem6  34094  cos9thpiminply  34095  cos9thpinconstrlem2  34097  trisecnconstr  34099  xrge0iifiso  34242  xrge0iifmhm  34246  xrge0pluscn  34247  rezh  34276  qqh0  34291  qqh1  34292  qqhcn  34298  qqhucn  34299  rerrext  34316  cnrrext  34317  mbfmvolf  34573  hgt750lem  34955  r1filimi  35411  r1filim  35412  r1omfi  35413  r1omhf  35414  r1omfv  35418  subfacval3  35552  erdszelem5  35558  erdszelem8  35561  filnetlem3  36753  filnetlem4  36754  bj-genr  37062  bj-genl  37063  bj-genan  37064  bj-rveccmod  37806  reheibor  38350  cossssid  39068  eqvrelcoss3  39213  3lexlogpow5ineq5  42689  aks6d1c7lem1  42809  tan3rdpi  42973  sin2t3rdpi  42974  sin4t3rdpi  42976  asin1half  42978  fourierdlem68  46746  fourierdlem77  46755  fourierdlem80  46758  fouriersw  46803  etransclem23  46829  gsumge0cl  46943  nthrucw  47460  abcdta  47517  abcdtb  47518  abcdtc  47519  nabctnabc  47523  ppivalnn4  48234  zlmodzxzsubm  48990  zlmodzxzldeplem3  49133  ldepsnlinclem1  49136  ldepsnlinclem2  49137  ldepsnlinc  49139  sepfsepc  49557  prstcleval  50184  prstcocval  50186  setc1onsubc  50231  empty-surprise  50411  amgmwlem  50431  amgmlemALT  50432