Theorem simpli 485

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

Syntax hints:   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  tfr2b  8393  rdgfun  8413  oeoa  8594  oeoe  8596  ssdomg  8993  ordtypelem4  9513  ordtypelem6  9515  ordtypelem7  9516  r1limg  9763  rankwflemb  9785  r1elssi  9797  infxpenlem  10005  ackbij2  10235  wunom  10712  mulnzcnopr  11857  negiso  12191  infrenegsup  12194  hashunlei  14382  hashsslei  14383  cos01bnd  16126  cos1bnd  16127  cos2bnd  16128  sin4lt0  16135  egt2lt3  16146  epos  16147  ene1  16150  divalglem5  16337  bitsf1o  16383  gcdaddmlem  16462  sravsca  20793  zrhpsgnmhm  21129  resubgval  21154  re1r  21158  redvr  21162  refld  21164  rzgrp  21168  txindis  23130  icopnfhmeo  24451  iccpnfcnv  24452  iccpnfhmeo  24453  xrhmeo  24454  cnheiborlem  24462  recvs  24654  recvsOLD  24655  qcvs  24656  rrxcph  24901  volf  25038  i1f1  25199  itg11  25200  dvsin  25491  taylthlem2  25878  reefgim  25954  pilem3  25957  pigt2lt4  25958  pire  25960  pipos  25962  sinhalfpi  25970  tan4thpi  26016  sincos3rdpi  26018  pigt3  26019  circgrp  26053  circsubm  26054  1cubrlem  26336  1cubr  26337  jensenlem2  26482  amgmlem  26484  emcllem6  26495  emcllem7  26496  harmonicbnd3  26502  ppiublem1  26695  chtub  26705  bposlem7  26783  lgsdir2lem4  26821  lgsdir2lem5  26822  chebbnd1  26965  mulog2sumlem2  27028  pntpbnd1a  27078  pntpbnd2  27080  pntlemb  27090  pntlemk  27099  qrng0  27114  qrng1  27115  qrngneg  27116  qrngdiv  27117  qabsabv  27122  ex-sqrt  29697  normlem7tALT  30360  hhsssh  30510  shintcli  30570  chintcli  30572  omlsi  30645  qlaxr3i  30877  lnophm  31260  nmcopex  31270  nmcoplb  31271  nmbdfnlbi  31290  nmcfnex  31294  nmcfnlb  31295  hmopidmch  31394  hmopidmpj  31395  chirred  31636  threehalves  32069  1fldgenq  32401  nn0archi  32451  ccfldextrr  32716  ccfldsrarelvec  32734  xrge0iifiso  32904  xrge0iifmhm  32908  xrge0pluscn  32909  rezh  32940  qqh0  32953  qqh1  32954  qqhcn  32960  qqhucn  32961  rerrext  32978  cnrrext  32979  mbfmvolf  33254  hgt750lem  33652  subfacval3  34169  erdszelem5  34175  erdszelem8  34178  filnetlem3  35254  filnetlem4  35255  bj-genr  35473  bj-genl  35474  bj-genan  35475  bj-rveccmod  36172  reheibor  36696  cossssid  37326  eqvrelcoss3  37477  3lexlogpow5ineq5  40914  fourierdlem68  44877  fourierdlem77  44886  fourierdlem80  44889  fouriersw  44934  etransclem23  44960  gsumge0cl  45074  abcdta  45622  abcdtb  45623  abcdtc  45624  nabctnabc  45628  zlmodzxzsubm  46989  zlmodzxzldeplem3  47137  ldepsnlinclem1  47140  ldepsnlinclem2  47141  ldepsnlinc  47143  sepfsepc  47514  prstcleval  47642  prstcocval  47645  empty-surprise  47783  amgmwlem  47803  amgmlemALT  47804