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  8327  rdgfun  8347  oeoa  8525  oeoe  8527  ssdomg  8937  ordtypelem4  9426  ordtypelem6  9428  ordtypelem7  9429  r1limg  9683  rankwflemb  9705  r1elssi  9717  infxpenlem  9923  ackbij2  10152  wunom  10631  mulnzcnf  11783  negiso  12122  infrenegsup  12125  hashunlei  14348  hashsslei  14349  cos01bnd  16111  cos1bnd  16112  cos2bnd  16113  sin4lt0  16120  egt2lt3  16131  epos  16132  ene1  16135  divalglem5  16324  bitsf1o  16372  gcdaddmlem  16451  sravsca  21133  zrhpsgnmhm  21539  resubgval  21564  re1r  21568  redvr  21572  refld  21574  rzgrp  21578  txindis  23578  icopnfhmeo  24897  iccpnfcnv  24898  iccpnfhmeo  24899  xrhmeo  24900  cnheiborlem  24909  recvs  25102  qcvs  25103  rrxcph  25348  volf  25486  i1f1  25647  itg11  25648  dvsin  25942  taylthlem2  26338  taylthlem2OLD  26339  reefgim  26416  pilem3  26419  pigt2lt4  26420  pire  26422  pipos  26424  sinhalfpi  26433  tan4thpi  26479  tan4thpiOLD  26480  sincos3rdpi  26482  pigt3  26483  circgrp  26517  circsubm  26518  1cubrlem  26807  1cubr  26808  jensenlem2  26954  amgmlem  26956  emcllem6  26967  emcllem7  26968  harmonicbnd3  26974  ppiublem1  27169  chtub  27179  bposlem7  27257  lgsdir2lem4  27295  lgsdir2lem5  27296  chebbnd1  27439  mulog2sumlem2  27502  pntpbnd1a  27552  pntpbnd2  27554  pntlemb  27564  pntlemk  27573  qrng0  27588  qrng1  27589  qrngneg  27590  qrngdiv  27591  qabsabv  27596  ex-sqrt  30529  normlem7tALT  31194  hhsssh  31344  shintcli  31404  chintcli  31406  omlsi  31479  qlaxr3i  31711  lnophm  32094  nmcopex  32104  nmcoplb  32105  nmbdfnlbi  32124  nmcfnex  32128  nmcfnlb  32129  hmopidmch  32228  hmopidmpj  32229  chirred  32470  threehalves  32996  qfld  33379  1fldgenq  33404  nn0archi  33428  ccfldextrr  33803  ccfldsrarelvec  33828  constrextdg2  33906  constrext2chnlem  33907  constrcon  33931  2sqr3minply  33937  2sqr3nconstr  33938  cos9thpiminplylem6  33944  cos9thpiminply  33945  cos9thpinconstrlem2  33947  trisecnconstr  33949  xrge0iifiso  34092  xrge0iifmhm  34096  xrge0pluscn  34097  rezh  34126  qqh0  34141  qqh1  34142  qqhcn  34148  qqhucn  34149  rerrext  34166  cnrrext  34167  mbfmvolf  34423  hgt750lem  34808  r1filimi  35259  r1filim  35260  r1omfi  35261  r1omhf  35262  r1omfv  35266  subfacval3  35383  erdszelem5  35389  erdszelem8  35392  filnetlem3  36574  filnetlem4  36575  bj-genr  36806  bj-genl  36807  bj-genan  36808  bj-rveccmod  37503  reheibor  38036  cossssid  38726  eqvrelcoss3  38871  3lexlogpow5ineq5  42310  aks6d1c7lem1  42430  tan3rdpi  42603  sin2t3rdpi  42604  sin4t3rdpi  42606  asin1half  42608  fourierdlem68  46414  fourierdlem77  46423  fourierdlem80  46426  fouriersw  46471  etransclem23  46497  gsumge0cl  46611  nthrucw  47126  abcdta  47167  abcdtb  47168  abcdtc  47169  nabctnabc  47173  zlmodzxzsubm  48601  zlmodzxzldeplem3  48744  ldepsnlinclem1  48747  ldepsnlinclem2  48748  ldepsnlinc  48750  sepfsepc  49169  prstcleval  49796  prstcocval  49798  setc1onsubc  49843  empty-surprise  50023  amgmwlem  50043  amgmlemALT  50044