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 196  df-an 385

This theorem is referenced by:  exan  1775  exanOLD  1776  pwundif  4945  tfr2b  7379  rdgfun  7399  oeoa  7564  oeoe  7566  ssdomg  7887  ordtypelem4  8309  ordtypelem6  8311  ordtypelem7  8312  r1limg  8517  rankwflemb  8539  r1elssi  8551  infxpenlem  8719  ackbij2  8948  wunom  9421  mulnzcnopr  10552  negiso  10880  infrenegsup  10883  hashunlei  13072  hashsslei  13073  cos01bnd  14755  cos1bnd  14756  cos2bnd  14757  sin4lt0  14764  egt2lt3  14773  epos  14774  ene1  14777  divalglem5  14958  bitsf1o  15005  gcdaddmlem  15083  strlemor1  15796  zrhpsgnmhm  19749  resubgval  19774  re1r  19778  redvr  19782  refld  19784  txindis  21247  icopnfhmeo  22550  iccpnfcnv  22551  iccpnfhmeo  22552  xrhmeo  22553  cnheiborlem  22561  recvs  22754  qcvs  22755  rrxcph  22988  volf  23104  i1f1  23263  itg11  23264  dvsin  23549  taylthlem2  23932  reefgim  24008  pilem3  24011  pigt2lt4  24012  pire  24014  pipos  24016  sinhalfpi  24024  tan4thpi  24070  sincos3rdpi  24072  circgrp  24102  circsubm  24103  rzgrp  24104  1cubrlem  24368  1cubr  24369  jensenlem2  24514  amgmlem  24516  emcllem6  24527  emcllem7  24528  emgt0  24533  harmonicbnd3  24534  ppiublem1  24727  chtub  24737  bposlem7  24815  lgsdir2lem4  24853  lgsdir2lem5  24854  chebbnd1  24961  mulog2sumlem2  25024  pntpbnd1a  25074  pntpbnd2  25076  pntlemb  25086  pntlemk  25095  qrng0  25110  qrng1  25111  qrngneg  25112  qrngdiv  25113  qabsabv  25118  2trllemE  26083  ex-sqrt  26703  normlem7tALT  27360  hhsssh  27510  shintcli  27572  chintcli  27574  omlsi  27647  qlaxr3i  27879  lnophm  28262  nmcopex  28272  nmcoplb  28273  nmbdfnlbi  28292  nmcfnex  28296  nmcfnlb  28297  hmopidmch  28396  hmopidmpj  28397  chirred  28638  nn0archi  29174  xrge0iifiso  29309  xrge0iifmhm  29313  xrge0pluscn  29314  rezh  29343  qqh0  29356  qqh1  29357  qqhcn  29363  qqhucn  29364  rerrext  29381  cnrrext  29382  mbfmvolf  29655  subfacval3  30425  erdszelem5  30431  erdszelem8  30434  filnetlem3  31545  filnetlem4  31546  bj-genr  31776  bj-genl  31777  bj-genan  31778  pigt3  32572  reheibor  32808  fourierdlem68  39067  fourierdlem77  39076  fourierdlem80  39079  fouriersw  39124  etransclem23  39150  gsumge0cl  39264  abcdta  39741  abcdtb  39742  abcdtc  39743  nabctnabc  39747  zlmodzxzsubm  41930  zlmodzxzldeplem3  42085  ldepsnlinclem1  42088  ldepsnlinclem2  42089  ldepsnlinc  42091  empty-surprise  42337  amgmwlem  42357  amgmlemALT  42358