Theorem simpli 489

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

This proof depends on syntax axioms:   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  tfr2b  8389  rdgfun  8409  oeoa  8589  oeoe  8591  ssdomg  9010  ordtypelem4  9497  ordtypelem6  9499  ordtypelem7  9500  r1limg  9757  rankwflemb  9779  r1elssi  9791  infxpenlem  10020  ackbij2  10248  wunom  10733  mulnzcnf  11888  negiso  12223  infrenegsup  12226  hashunlei  14494  hashsslei  14495  cos01bnd  16280  cos1bnd  16281  cos2bnd  16282  sin4lt0  16289  egt2lt3  16300  epos  16301  ene1  16304  divalglem5  16493  bitsf1o  16541  gcdaddmlem  16620  sravsca  21371  zrhpsgnmhm  21803  resubgval  21828  re1r  21832  redvr  21836  refld  21838  rzgrp  21842  txindis  23866  icopnfhmeo  25177  iccpnfcnv  25178  iccpnfhmeo  25179  xrhmeo  25180  cnheiborlem  25188  recvs  25380  qcvs  25381  rrxcph  25626  volf  25763  i1f1  25924  itg11  25925  dvsin  26216  taylthlem2  26617  reefgim  26693  pilem3  26696  pigt2lt4  26697  pire  26699  pipos  26703  sinhalfpi  26713  tan4thpi  26759  tan4thpiOLD  26760  sincos3rdpi  26762  pigt3  26763  circgrp  26797  circsubm  26798  1cubrlem  27086  1cubr  27087  jensenlem2  27232  amgmlem  27234  emcllem6  27245  emcllem7  27246  harmonicbnd3  27252  ppiublem1  27446  chtub  27456  bposlem7  27534  lgsdir2lem4  27572  lgsdir2lem5  27573  chebbnd1  27716  mulog2sumlem2  27779  pntpbnd1a  27829  pntpbnd2  27831  pntlemb  27841  pntlemk  27850  qrng0  27865  qrng1  27866  qrngneg  27867  qrngdiv  27868  qabsabv  27873  ex-sqrt  30942  normlem7tALT  31608  hhsssh  31758  shintcli  31818  chintcli  31820  omlsi  31893  qlaxr3i  32125  lnophm  32508  nmcopex  32518  nmcoplb  32519  nmbdfnlbi  32538  nmcfnex  32542  nmcfnlb  32543  hmopidmch  32642  hmopidmpj  32643  chirred  32884  threehalves  33368  qfld  33746  1fldgenq  33771  nn0archi  33795  ccfldextrr  34164  ccfldsrarelvec  34189  constrextdg2  34267  constrext2chnlem  34268  constrcon  34292  2sqr3minply  34298  2sqr3nconstr  34299  cos9thpiminplylem6  34305  cos9thpiminply  34306  cos9thpinconstrlem2  34308  trisecnconstr  34310  xrge0iifiso  34453  xrge0iifmhm  34457  xrge0pluscn  34458  rezh  34487  qqh0  34502  qqh1  34503  qqhcn  34509  qqhucn  34510  rerrext  34527  cnrrext  34528  mbfmvolf  34785  hgt750lem  35167  r1filimi  35619  r1filim  35620  r1omfi  35621  r1omhf  35622  r1omfv  35626  subfacval3  35776  erdszelem5  35782  erdszelem8  35785  filnetlem3  37007  filnetlem4  37008  bj-genr  37316  bj-genl  37317  bj-genan  37318  bj-rveccmod  38062  reheibor  38597  cossssid  39313  eqvrelcoss3  39458  3lexlogpow5ineq5  42934  aks6d1c7lem1  43054  tan3rdpi  43235  sin2t3rdpi  43236  sin4t3rdpi  43238  asin1half  43240  fourierdlem68  47010  fourierdlem77  47019  fourierdlem80  47022  fouriersw  47067  etransclem23  47093  gsumge0cl  47207  numtowerdt  47742  abcdta  47821  abcdtb  47822  abcdtc  47823  nabctnabc  47827  ppivalnn4  48538  zlmodzxzsubm  49297  zlmodzxzldeplem3  49440  ldepsnlinclem1  49443  ldepsnlinclem2  49444  ldepsnlinc  49446  sepfsepc  49862  prstcleval  50489  prstcocval  50491  setc1onsubc  50536  empty-surprise  50719  veroquadmodzerod  50825  veroquadnolindfd  50826  veroquaddetzerod  50827  amgmwlem  50828  amgmlemALT  50829