Theorem simpli 486

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

Syntax hints:   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  exanOLD  1863  pwundifOLD  5459  tfr2b  8034  rdgfun  8054  oeoa  8225  oeoe  8227  ssdomg  8557  ordtypelem4  8987  ordtypelem6  8989  ordtypelem7  8990  r1limg  9202  rankwflemb  9224  r1elssi  9236  infxpenlem  9441  ackbij2  9667  wunom  10144  mulnzcnopr  11288  negiso  11623  infrenegsup  11626  hashunlei  13789  hashsslei  13790  cos01bnd  15541  cos1bnd  15542  cos2bnd  15543  sin4lt0  15550  egt2lt3  15561  epos  15562  ene1  15565  divalglem5  15750  bitsf1o  15796  gcdaddmlem  15874  zrhpsgnmhm  20730  resubgval  20755  re1r  20759  redvr  20763  refld  20765  rzgrp  20769  txindis  22244  icopnfhmeo  23549  iccpnfcnv  23550  iccpnfhmeo  23551  xrhmeo  23552  cnheiborlem  23560  recvs  23752  qcvs  23753  rrxcph  23997  volf  24132  i1f1  24293  itg11  24294  dvsin  24581  taylthlem2  24964  reefgim  25040  pilem3  25043  pigt2lt4  25044  pire  25046  pipos  25048  sinhalfpi  25056  tan4thpi  25102  sincos3rdpi  25104  pigt3  25105  circgrp  25138  circsubm  25139  1cubrlem  25421  1cubr  25422  jensenlem2  25567  amgmlem  25569  emcllem6  25580  emcllem7  25581  harmonicbnd3  25587  ppiublem1  25780  chtub  25790  bposlem7  25868  lgsdir2lem4  25906  lgsdir2lem5  25907  chebbnd1  26050  mulog2sumlem2  26113  pntpbnd1a  26163  pntpbnd2  26165  pntlemb  26175  pntlemk  26184  qrng0  26199  qrng1  26200  qrngneg  26201  qrngdiv  26202  qabsabv  26207  ex-sqrt  28235  normlem7tALT  28898  hhsssh  29048  shintcli  29108  chintcli  29110  omlsi  29183  qlaxr3i  29415  lnophm  29798  nmcopex  29808  nmcoplb  29809  nmbdfnlbi  29828  nmcfnex  29832  nmcfnlb  29833  hmopidmch  29932  hmopidmpj  29933  chirred  30174  threehalves  30593  nn0archi  30918  ccfldextrr  31040  ccfldsrarelvec  31058  xrge0iifiso  31180  xrge0iifmhm  31184  xrge0pluscn  31185  rezh  31214  qqh0  31227  qqh1  31228  qqhcn  31234  qqhucn  31235  rerrext  31252  cnrrext  31253  mbfmvolf  31526  hgt750lem  31924  subfacval3  32438  erdszelem5  32444  erdszelem8  32447  filnetlem3  33730  filnetlem4  33731  bj-genr  33942  bj-genl  33943  bj-genan  33944  bj-rveccmod  34585  reheibor  35119  cossssid  35709  eqvrelcoss3  35855  fourierdlem68  42466  fourierdlem77  42475  fourierdlem80  42478  fouriersw  42523  etransclem23  42549  gsumge0cl  42660  abcdta  43168  abcdtb  43169  abcdtc  43170  nabctnabc  43174  zlmodzxzsubm  44414  zlmodzxzldeplem3  44564  ldepsnlinclem1  44567  ldepsnlinclem2  44568  ldepsnlinc  44570  empty-surprise  44890  amgmwlem  44910  amgmlemALT  44911