Theorem simpli 474

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

Syntax hints:   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  exan  1788  exanOLD  1789  pwundif  5021  tfr2b  7492  rdgfun  7512  oeoa  7677  oeoe  7679  ssdomg  8001  ordtypelem4  8426  ordtypelem6  8428  ordtypelem7  8429  r1limg  8634  rankwflemb  8656  r1elssi  8668  infxpenlem  8836  ackbij2  9065  wunom  9542  mulnzcnopr  10673  negiso  11003  infrenegsup  11006  hashunlei  13212  hashsslei  13213  cos01bnd  14916  cos1bnd  14917  cos2bnd  14918  sin4lt0  14925  egt2lt3  14934  epos  14935  ene1  14938  divalglem5  15120  bitsf1o  15167  gcdaddmlem  15245  strlemor1OLD  15969  zrhpsgnmhm  19930  resubgval  19955  re1r  19959  redvr  19963  refld  19965  txindis  21437  icopnfhmeo  22742  iccpnfcnv  22743  iccpnfhmeo  22744  xrhmeo  22745  cnheiborlem  22753  recvs  22946  qcvs  22947  rrxcph  23180  volf  23297  i1f1  23457  itg11  23458  dvsin  23745  taylthlem2  24128  reefgim  24204  pilem3  24207  pigt2lt4  24208  pire  24210  pipos  24212  sinhalfpi  24220  tan4thpi  24266  sincos3rdpi  24268  circgrp  24298  circsubm  24299  rzgrp  24300  1cubrlem  24568  1cubr  24569  jensenlem2  24714  amgmlem  24716  emcllem6  24727  emcllem7  24728  emgt0  24733  harmonicbnd3  24734  ppiublem1  24927  chtub  24937  bposlem7  25015  lgsdir2lem4  25053  lgsdir2lem5  25054  chebbnd1  25161  mulog2sumlem2  25224  pntpbnd1a  25274  pntpbnd2  25276  pntlemb  25286  pntlemk  25295  qrng0  25310  qrng1  25311  qrngneg  25312  qrngdiv  25313  qabsabv  25318  ex-sqrt  27311  normlem7tALT  27976  hhsssh  28126  shintcli  28188  chintcli  28190  omlsi  28263  qlaxr3i  28495  lnophm  28878  nmcopex  28888  nmcoplb  28889  nmbdfnlbi  28908  nmcfnex  28912  nmcfnlb  28913  hmopidmch  29012  hmopidmpj  29013  chirred  29254  threehalves  29623  nn0archi  29843  xrge0iifiso  29981  xrge0iifmhm  29985  xrge0pluscn  29986  rezh  30015  qqh0  30028  qqh1  30029  qqhcn  30035  qqhucn  30036  rerrext  30053  cnrrext  30054  mbfmvolf  30328  hgt750lem  30729  subfacval3  31171  erdszelem5  31177  erdszelem8  31180  filnetlem3  32375  filnetlem4  32376  bj-genr  32591  bj-genl  32592  bj-genan  32593  pigt3  33402  reheibor  33638  fourierdlem68  40391  fourierdlem77  40400  fourierdlem80  40403  fouriersw  40448  etransclem23  40474  gsumge0cl  40588  abcdta  41092  abcdtb  41093  abcdtc  41094  nabctnabc  41098  zlmodzxzsubm  42137  zlmodzxzldeplem3  42291  ldepsnlinclem1  42294  ldepsnlinclem2  42295  ldepsnlinc  42297  empty-surprise  42528  amgmwlem  42548  amgmlemALT  42549