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  8337  rdgfun  8357  oeoa  8535  oeoe  8537  ssdomg  8949  ordtypelem4  9438  ordtypelem6  9440  ordtypelem7  9441  r1limg  9695  rankwflemb  9717  r1elssi  9729  infxpenlem  9935  ackbij2  10164  wunom  10643  mulnzcnf  11795  negiso  12134  infrenegsup  12137  hashunlei  14360  hashsslei  14361  cos01bnd  16123  cos1bnd  16124  cos2bnd  16125  sin4lt0  16132  egt2lt3  16143  epos  16144  ene1  16147  divalglem5  16336  bitsf1o  16384  gcdaddmlem  16463  sravsca  21145  zrhpsgnmhm  21551  resubgval  21576  re1r  21580  redvr  21584  refld  21586  rzgrp  21590  txindis  23590  icopnfhmeo  24909  iccpnfcnv  24910  iccpnfhmeo  24911  xrhmeo  24912  cnheiborlem  24921  recvs  25114  qcvs  25115  rrxcph  25360  volf  25498  i1f1  25659  itg11  25660  dvsin  25954  taylthlem2  26350  taylthlem2OLD  26351  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  26819  1cubr  26820  jensenlem2  26966  amgmlem  26968  emcllem6  26979  emcllem7  26980  harmonicbnd3  26986  ppiublem1  27181  chtub  27191  bposlem7  27269  lgsdir2lem4  27307  lgsdir2lem5  27308  chebbnd1  27451  mulog2sumlem2  27514  pntpbnd1a  27564  pntpbnd2  27566  pntlemb  27576  pntlemk  27585  qrng0  27600  qrng1  27601  qrngneg  27602  qrngdiv  27603  qabsabv  27608  ex-sqrt  30541  normlem7tALT  31206  hhsssh  31356  shintcli  31416  chintcli  31418  omlsi  31491  qlaxr3i  31723  lnophm  32106  nmcopex  32116  nmcoplb  32117  nmbdfnlbi  32136  nmcfnex  32140  nmcfnlb  32141  hmopidmch  32240  hmopidmpj  32241  chirred  32482  threehalves  33006  qfld  33390  1fldgenq  33415  nn0archi  33439  ccfldextrr  33823  ccfldsrarelvec  33848  constrextdg2  33926  constrext2chnlem  33927  constrcon  33951  2sqr3minply  33957  2sqr3nconstr  33958  cos9thpiminplylem6  33964  cos9thpiminply  33965  cos9thpinconstrlem2  33967  trisecnconstr  33969  xrge0iifiso  34112  xrge0iifmhm  34116  xrge0pluscn  34117  rezh  34146  qqh0  34161  qqh1  34162  qqhcn  34168  qqhucn  34169  rerrext  34186  cnrrext  34187  mbfmvolf  34443  hgt750lem  34828  r1filimi  35278  r1filim  35279  r1omfi  35280  r1omhf  35281  r1omfv  35285  subfacval3  35402  erdszelem5  35408  erdszelem8  35411  filnetlem3  36593  filnetlem4  36594  bj-genr  36828  bj-genl  36829  bj-genan  36830  bj-rveccmod  37551  reheibor  38084  cossssid  38802  eqvrelcoss3  38947  3lexlogpow5ineq5  42424  aks6d1c7lem1  42544  tan3rdpi  42716  sin2t3rdpi  42717  sin4t3rdpi  42719  asin1half  42721  fourierdlem68  46526  fourierdlem77  46535  fourierdlem80  46538  fouriersw  46583  etransclem23  46609  gsumge0cl  46723  nthrucw  47238  abcdta  47279  abcdtb  47280  abcdtc  47281  nabctnabc  47285  zlmodzxzsubm  48713  zlmodzxzldeplem3  48856  ldepsnlinclem1  48859  ldepsnlinclem2  48860  ldepsnlinc  48862  sepfsepc  49281  prstcleval  49908  prstcocval  49910  setc1onsubc  49955  empty-surprise  50135  amgmwlem  50155  amgmlemALT  50156