Theorem simpli 489

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

This proof depends on syntax axioms:   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  tfr2b  8392  rdgfun  8412  oeoa  8592  oeoe  8594  ssdomg  9006  ordtypelem4  9493  ordtypelem6  9495  ordtypelem7  9496  r1limg  9753  rankwflemb  9775  r1elssi  9787  infxpenlem  10016  ackbij2  10244  wunom  10723  mulnzcnf  11878  negiso  12213  infrenegsup  12216  hashunlei  14482  hashsslei  14483  cos01bnd  16267  cos1bnd  16268  cos2bnd  16269  sin4lt0  16276  egt2lt3  16287  epos  16288  ene1  16291  divalglem5  16480  bitsf1o  16528  gcdaddmlem  16607  sravsca  21339  zrhpsgnmhm  21771  resubgval  21796  re1r  21800  redvr  21804  refld  21806  rzgrp  21810  txindis  23828  icopnfhmeo  25139  iccpnfcnv  25140  iccpnfhmeo  25141  xrhmeo  25142  cnheiborlem  25150  recvs  25342  qcvs  25343  rrxcph  25588  volf  25725  i1f1  25886  itg11  25887  dvsin  26178  taylthlem2  26574  reefgim  26650  pilem3  26653  pigt2lt4  26654  pire  26656  pipos  26660  sinhalfpi  26670  tan4thpi  26716  tan4thpiOLD  26717  sincos3rdpi  26719  pigt3  26720  circgrp  26754  circsubm  26755  1cubrlem  27043  1cubr  27044  jensenlem2  27189  amgmlem  27191  emcllem6  27202  emcllem7  27203  harmonicbnd3  27209  ppiublem1  27403  chtub  27413  bposlem7  27491  lgsdir2lem4  27529  lgsdir2lem5  27530  chebbnd1  27673  mulog2sumlem2  27736  pntpbnd1a  27786  pntpbnd2  27788  pntlemb  27798  pntlemk  27807  qrng0  27822  qrng1  27823  qrngneg  27824  qrngdiv  27825  qabsabv  27830  ex-sqrt  30842  normlem7tALT  31508  hhsssh  31658  shintcli  31718  chintcli  31720  omlsi  31793  qlaxr3i  32025  lnophm  32408  nmcopex  32418  nmcoplb  32419  nmbdfnlbi  32438  nmcfnex  32442  nmcfnlb  32443  hmopidmch  32542  hmopidmpj  32543  chirred  32784  threehalves  33271  qfld  33649  1fldgenq  33674  nn0archi  33698  ccfldextrr  34067  ccfldsrarelvec  34092  constrextdg2  34170  constrext2chnlem  34171  constrcon  34195  2sqr3minply  34201  2sqr3nconstr  34202  cos9thpiminplylem6  34208  cos9thpiminply  34209  cos9thpinconstrlem2  34211  trisecnconstr  34213  xrge0iifiso  34356  xrge0iifmhm  34360  xrge0pluscn  34361  rezh  34390  qqh0  34405  qqh1  34406  qqhcn  34412  qqhucn  34413  rerrext  34430  cnrrext  34431  mbfmvolf  34688  hgt750lem  35070  r1filimi  35522  r1filim  35523  r1omfi  35524  r1omhf  35525  r1omfv  35529  subfacval3  35702  erdszelem5  35708  erdszelem8  35711  filnetlem3  36932  filnetlem4  36933  bj-genr  37241  bj-genl  37242  bj-genan  37243  bj-rveccmod  37987  reheibor  38531  cossssid  39247  eqvrelcoss3  39392  3lexlogpow5ineq5  42868  aks6d1c7lem1  42988  tan3rdpi  43154  sin2t3rdpi  43155  sin4t3rdpi  43157  asin1half  43159  fourierdlem68  46929  fourierdlem77  46938  fourierdlem80  46941  fouriersw  46986  etransclem23  47012  gsumge0cl  47126  nthrucw  47648  abcdta  47703  abcdtb  47704  abcdtc  47705  nabctnabc  47709  ppivalnn4  48420  zlmodzxzsubm  49180  zlmodzxzldeplem3  49323  ldepsnlinclem1  49326  ldepsnlinclem2  49327  ldepsnlinc  49329  sepfsepc  49747  prstcleval  50374  prstcocval  50376  setc1onsubc  50421  empty-surprise  50601  amgmwlem  50691  amgmlemALT  50692