Theorem simpli 487

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

Syntax hints:   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  pwundifOLD  5452  tfr2b  8132  rdgfun  8152  oeoa  8325  oeoe  8327  ssdomg  8674  ordtypelem4  9137  ordtypelem6  9139  ordtypelem7  9140  r1limg  9387  rankwflemb  9409  r1elssi  9421  infxpenlem  9627  ackbij2  9857  wunom  10334  mulnzcnopr  11478  negiso  11812  infrenegsup  11815  hashunlei  13992  hashsslei  13993  cos01bnd  15747  cos1bnd  15748  cos2bnd  15749  sin4lt0  15756  egt2lt3  15767  epos  15768  ene1  15771  divalglem5  15958  bitsf1o  16004  gcdaddmlem  16083  zrhpsgnmhm  20546  resubgval  20571  re1r  20575  redvr  20579  refld  20581  rzgrp  20585  txindis  22531  icopnfhmeo  23840  iccpnfcnv  23841  iccpnfhmeo  23842  xrhmeo  23843  cnheiborlem  23851  recvs  24043  qcvs  24044  rrxcph  24289  volf  24426  i1f1  24587  itg11  24588  dvsin  24879  taylthlem2  25266  reefgim  25342  pilem3  25345  pigt2lt4  25346  pire  25348  pipos  25350  sinhalfpi  25358  tan4thpi  25404  sincos3rdpi  25406  pigt3  25407  circgrp  25441  circsubm  25442  1cubrlem  25724  1cubr  25725  jensenlem2  25870  amgmlem  25872  emcllem6  25883  emcllem7  25884  harmonicbnd3  25890  ppiublem1  26083  chtub  26093  bposlem7  26171  lgsdir2lem4  26209  lgsdir2lem5  26210  chebbnd1  26353  mulog2sumlem2  26416  pntpbnd1a  26466  pntpbnd2  26468  pntlemb  26478  pntlemk  26487  qrng0  26502  qrng1  26503  qrngneg  26504  qrngdiv  26505  qabsabv  26510  ex-sqrt  28537  normlem7tALT  29200  hhsssh  29350  shintcli  29410  chintcli  29412  omlsi  29485  qlaxr3i  29717  lnophm  30100  nmcopex  30110  nmcoplb  30111  nmbdfnlbi  30130  nmcfnex  30134  nmcfnlb  30135  hmopidmch  30234  hmopidmpj  30235  chirred  30476  threehalves  30909  nn0archi  31261  ccfldextrr  31437  ccfldsrarelvec  31455  xrge0iifiso  31599  xrge0iifmhm  31603  xrge0pluscn  31604  rezh  31633  qqh0  31646  qqh1  31647  qqhcn  31653  qqhucn  31654  rerrext  31671  cnrrext  31672  mbfmvolf  31945  hgt750lem  32343  subfacval3  32864  erdszelem5  32870  erdszelem8  32873  filnetlem3  34306  filnetlem4  34307  bj-genr  34525  bj-genl  34526  bj-genan  34527  bj-rveccmod  35207  reheibor  35734  cossssid  36322  eqvrelcoss3  36468  3lexlogpow5ineq5  39802  fourierdlem68  43390  fourierdlem77  43399  fourierdlem80  43402  fouriersw  43447  etransclem23  43473  gsumge0cl  43584  abcdta  44092  abcdtb  44093  abcdtc  44094  nabctnabc  44098  zlmodzxzsubm  45368  zlmodzxzldeplem3  45516  ldepsnlinclem1  45519  ldepsnlinclem2  45520  ldepsnlinc  45522  sepfsepc  45894  empty-surprise  46157  amgmwlem  46177  amgmlemALT  46178