Theorem simpli 483

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

Syntax hints:   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  tfr2b  8321  rdgfun  8341  oeoa  8518  oeoe  8520  ssdomg  8929  ordtypelem4  9414  ordtypelem6  9416  ordtypelem7  9417  r1limg  9671  rankwflemb  9693  r1elssi  9705  infxpenlem  9911  ackbij2  10140  wunom  10618  mulnzcnf  11770  negiso  12109  infrenegsup  12112  hashunlei  14334  hashsslei  14335  cos01bnd  16097  cos1bnd  16098  cos2bnd  16099  sin4lt0  16106  egt2lt3  16117  epos  16118  ene1  16121  divalglem5  16310  bitsf1o  16358  gcdaddmlem  16437  sravsca  21117  zrhpsgnmhm  21523  resubgval  21548  re1r  21552  redvr  21556  refld  21558  rzgrp  21562  txindis  23550  icopnfhmeo  24869  iccpnfcnv  24870  iccpnfhmeo  24871  xrhmeo  24872  cnheiborlem  24881  recvs  25074  qcvs  25075  rrxcph  25320  volf  25458  i1f1  25619  itg11  25620  dvsin  25914  taylthlem2  26310  taylthlem2OLD  26311  reefgim  26388  pilem3  26391  pigt2lt4  26392  pire  26394  pipos  26396  sinhalfpi  26405  tan4thpi  26451  tan4thpiOLD  26452  sincos3rdpi  26454  pigt3  26455  circgrp  26489  circsubm  26490  1cubrlem  26779  1cubr  26780  jensenlem2  26926  amgmlem  26928  emcllem6  26939  emcllem7  26940  harmonicbnd3  26946  ppiublem1  27141  chtub  27151  bposlem7  27229  lgsdir2lem4  27267  lgsdir2lem5  27268  chebbnd1  27411  mulog2sumlem2  27474  pntpbnd1a  27524  pntpbnd2  27526  pntlemb  27536  pntlemk  27545  qrng0  27560  qrng1  27561  qrngneg  27562  qrngdiv  27563  qabsabv  27568  ex-sqrt  30436  normlem7tALT  31101  hhsssh  31251  shintcli  31311  chintcli  31313  omlsi  31386  qlaxr3i  31618  lnophm  32001  nmcopex  32011  nmcoplb  32012  nmbdfnlbi  32031  nmcfnex  32035  nmcfnlb  32036  hmopidmch  32135  hmopidmpj  32136  chirred  32377  threehalves  32902  qfld  33270  1fldgenq  33295  nn0archi  33319  ccfldextrr  33680  ccfldsrarelvec  33705  constrextdg2  33783  constrext2chnlem  33784  constrcon  33808  2sqr3minply  33814  2sqr3nconstr  33815  cos9thpiminplylem6  33821  cos9thpiminply  33822  cos9thpinconstrlem2  33824  trisecnconstr  33826  xrge0iifiso  33969  xrge0iifmhm  33973  xrge0pluscn  33974  rezh  34003  qqh0  34018  qqh1  34019  qqhcn  34025  qqhucn  34026  rerrext  34043  cnrrext  34044  mbfmvolf  34300  hgt750lem  34685  r1filimi  35135  r1filim  35136  r1omfi  35137  r1omhf  35138  r1omfv  35142  subfacval3  35254  erdszelem5  35260  erdszelem8  35263  filnetlem3  36445  filnetlem4  36446  bj-genr  36671  bj-genl  36672  bj-genan  36673  bj-rveccmod  37367  reheibor  37900  cossssid  38590  eqvrelcoss3  38735  3lexlogpow5ineq5  42174  aks6d1c7lem1  42294  tan3rdpi  42471  sin2t3rdpi  42472  sin4t3rdpi  42474  asin1half  42476  fourierdlem68  46297  fourierdlem77  46306  fourierdlem80  46309  fouriersw  46354  etransclem23  46380  gsumge0cl  46494  nthrucw  47009  abcdta  47050  abcdtb  47051  abcdtc  47052  nabctnabc  47056  zlmodzxzsubm  48484  zlmodzxzldeplem3  48628  ldepsnlinclem1  48631  ldepsnlinclem2  48632  ldepsnlinc  48634  sepfsepc  49053  prstcleval  49681  prstcocval  49683  setc1onsubc  49728  empty-surprise  49908  amgmwlem  49928  amgmlemALT  49929