Theorem simpli 473

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

Syntax hints:   ∧ wa 383

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 385

This theorem is referenced by:  exan  1828  exanOLD  1829  pwundif  5050  tfr2b  7537  rdgfun  7557  oeoa  7722  oeoe  7724  ssdomg  8043  ordtypelem4  8467  ordtypelem6  8469  ordtypelem7  8470  r1limg  8672  rankwflemb  8694  r1elssi  8706  infxpenlem  8874  ackbij2  9103  wunom  9580  mulnzcnopr  10711  negiso  11041  infrenegsup  11044  hashunlei  13250  hashsslei  13251  cos01bnd  14960  cos1bnd  14961  cos2bnd  14962  sin4lt0  14969  egt2lt3  14978  epos  14979  ene1  14982  divalglem5  15167  bitsf1o  15214  gcdaddmlem  15292  strlemor1OLD  16016  zrhpsgnmhm  19978  resubgval  20003  re1r  20007  redvr  20011  refld  20013  txindis  21485  icopnfhmeo  22789  iccpnfcnv  22790  iccpnfhmeo  22791  xrhmeo  22792  cnheiborlem  22800  recvs  22992  qcvs  22993  rrxcph  23226  volf  23343  i1f1  23502  itg11  23503  dvsin  23790  taylthlem2  24173  reefgim  24249  pilem3  24252  pigt2lt4  24253  pire  24255  pipos  24257  sinhalfpi  24265  tan4thpi  24311  sincos3rdpi  24313  circgrp  24343  circsubm  24344  rzgrp  24345  1cubrlem  24613  1cubr  24614  jensenlem2  24759  amgmlem  24761  emcllem6  24772  emcllem7  24773  emgt0  24778  harmonicbnd3  24779  ppiublem1  24972  chtub  24982  bposlem7  25060  lgsdir2lem4  25098  lgsdir2lem5  25099  chebbnd1  25206  mulog2sumlem2  25269  pntpbnd1a  25319  pntpbnd2  25321  pntlemb  25331  pntlemk  25340  qrng0  25355  qrng1  25356  qrngneg  25357  qrngdiv  25358  qabsabv  25363  ex-sqrt  27441  normlem7tALT  28104  hhsssh  28254  shintcli  28316  chintcli  28318  omlsi  28391  qlaxr3i  28623  lnophm  29006  nmcopex  29016  nmcoplb  29017  nmbdfnlbi  29036  nmcfnex  29040  nmcfnlb  29041  hmopidmch  29140  hmopidmpj  29141  chirred  29382  threehalves  29751  nn0archi  29971  xrge0iifiso  30109  xrge0iifmhm  30113  xrge0pluscn  30114  rezh  30143  qqh0  30156  qqh1  30157  qqhcn  30163  qqhucn  30164  rerrext  30181  cnrrext  30182  mbfmvolf  30456  hgt750lem  30857  subfacval3  31297  erdszelem5  31303  erdszelem8  31306  filnetlem3  32500  filnetlem4  32501  bj-genr  32716  bj-genl  32717  bj-genan  32718  pigt3  33532  reheibor  33768  cossssid  34357  fourierdlem68  40709  fourierdlem77  40718  fourierdlem80  40721  fouriersw  40766  etransclem23  40792  gsumge0cl  40906  abcdta  41413  abcdtb  41414  abcdtc  41415  nabctnabc  41419  zlmodzxzsubm  42462  zlmodzxzldeplem3  42616  ldepsnlinclem1  42619  ldepsnlinclem2  42620  ldepsnlinc  42622  empty-surprise  42856  amgmwlem  42876  amgmlemALT  42877