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  8328  rdgfun  8348  oeoa  8526  oeoe  8528  ssdomg  8940  ordtypelem4  9429  ordtypelem6  9431  ordtypelem7  9432  r1limg  9686  rankwflemb  9708  r1elssi  9720  infxpenlem  9926  ackbij2  10155  wunom  10634  mulnzcnf  11787  negiso  12127  infrenegsup  12130  hashunlei  14378  hashsslei  14379  cos01bnd  16144  cos1bnd  16145  cos2bnd  16146  sin4lt0  16153  egt2lt3  16164  epos  16165  ene1  16168  divalglem5  16357  bitsf1o  16405  gcdaddmlem  16484  sravsca  21168  zrhpsgnmhm  21574  resubgval  21599  re1r  21603  redvr  21607  refld  21609  rzgrp  21613  txindis  23609  icopnfhmeo  24920  iccpnfcnv  24921  iccpnfhmeo  24922  xrhmeo  24923  cnheiborlem  24931  recvs  25123  qcvs  25124  rrxcph  25369  volf  25506  i1f1  25667  itg11  25668  dvsin  25959  taylthlem2  26351  taylthlem2OLD  26352  reefgim  26428  pilem3  26431  pigt2lt4  26432  pire  26434  pipos  26436  sinhalfpi  26445  tan4thpi  26491  tan4thpiOLD  26492  sincos3rdpi  26494  pigt3  26495  circgrp  26529  circsubm  26530  1cubrlem  26818  1cubr  26819  jensenlem2  26965  amgmlem  26967  emcllem6  26978  emcllem7  26979  harmonicbnd3  26985  ppiublem1  27179  chtub  27189  bposlem7  27267  lgsdir2lem4  27305  lgsdir2lem5  27306  chebbnd1  27449  mulog2sumlem2  27512  pntpbnd1a  27562  pntpbnd2  27564  pntlemb  27574  pntlemk  27583  qrng0  27598  qrng1  27599  qrngneg  27600  qrngdiv  27601  qabsabv  27606  ex-sqrt  30539  normlem7tALT  31205  hhsssh  31355  shintcli  31415  chintcli  31417  omlsi  31490  qlaxr3i  31722  lnophm  32105  nmcopex  32115  nmcoplb  32116  nmbdfnlbi  32135  nmcfnex  32139  nmcfnlb  32140  hmopidmch  32239  hmopidmpj  32240  chirred  32481  threehalves  32989  qfld  33373  1fldgenq  33398  nn0archi  33422  ccfldextrr  33806  ccfldsrarelvec  33831  constrextdg2  33909  constrext2chnlem  33910  constrcon  33934  2sqr3minply  33940  2sqr3nconstr  33941  cos9thpiminplylem6  33947  cos9thpiminply  33948  cos9thpinconstrlem2  33950  trisecnconstr  33952  xrge0iifiso  34095  xrge0iifmhm  34099  xrge0pluscn  34100  rezh  34129  qqh0  34144  qqh1  34145  qqhcn  34151  qqhucn  34152  rerrext  34169  cnrrext  34170  mbfmvolf  34426  hgt750lem  34811  r1filimi  35262  r1filim  35263  r1omfi  35264  r1omhf  35265  r1omfv  35270  subfacval3  35387  erdszelem5  35393  erdszelem8  35396  filnetlem3  36578  filnetlem4  36579  bj-genr  36888  bj-genl  36889  bj-genan  36890  bj-rveccmod  37632  reheibor  38174  cossssid  38892  eqvrelcoss3  39037  3lexlogpow5ineq5  42513  aks6d1c7lem1  42633  tan3rdpi  42798  sin2t3rdpi  42799  sin4t3rdpi  42801  asin1half  42803  fourierdlem68  46620  fourierdlem77  46629  fourierdlem80  46632  fouriersw  46677  etransclem23  46703  gsumge0cl  46817  nthrucw  47332  abcdta  47385  abcdtb  47386  abcdtc  47387  nabctnabc  47391  ppivalnn4  48102  zlmodzxzsubm  48847  zlmodzxzldeplem3  48990  ldepsnlinclem1  48993  ldepsnlinclem2  48994  ldepsnlinc  48996  sepfsepc  49415  prstcleval  50042  prstcocval  50044  setc1onsubc  50089  empty-surprise  50269  amgmwlem  50289  amgmlemALT  50290