Theorem simpli 484

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

Syntax hints:   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  tfr2b  8332  rdgfun  8352  oeoa  8530  oeoe  8532  ssdomg  8944  ordtypelem4  9433  ordtypelem6  9435  ordtypelem7  9436  r1limg  9693  rankwflemb  9715  r1elssi  9727  infxpenlem  9933  ackbij2  10162  wunom  10641  mulnzcnf  11794  negiso  12134  infrenegsup  12137  hashunlei  14385  hashsslei  14386  cos01bnd  16151  cos1bnd  16152  cos2bnd  16153  sin4lt0  16160  egt2lt3  16171  epos  16172  ene1  16175  divalglem5  16364  bitsf1o  16412  gcdaddmlem  16491  sravsca  21178  zrhpsgnmhm  21566  resubgval  21591  re1r  21595  redvr  21599  refld  21601  rzgrp  21605  txindis  23624  icopnfhmeo  24935  iccpnfcnv  24936  iccpnfhmeo  24937  xrhmeo  24938  cnheiborlem  24946  recvs  25138  qcvs  25139  rrxcph  25384  volf  25521  i1f1  25682  itg11  25683  dvsin  25974  taylthlem2  26364  reefgim  26440  pilem3  26443  pigt2lt4  26444  pire  26446  pipos  26448  sinhalfpi  26457  tan4thpi  26503  tan4thpiOLD  26504  sincos3rdpi  26506  pigt3  26507  circgrp  26541  circsubm  26542  1cubrlem  26830  1cubr  26831  jensenlem2  26976  amgmlem  26978  emcllem6  26989  emcllem7  26990  harmonicbnd3  26996  ppiublem1  27190  chtub  27200  bposlem7  27278  lgsdir2lem4  27316  lgsdir2lem5  27317  chebbnd1  27460  mulog2sumlem2  27523  pntpbnd1a  27573  pntpbnd2  27575  pntlemb  27585  pntlemk  27594  qrng0  27609  qrng1  27610  qrngneg  27611  qrngdiv  27612  qabsabv  27617  ex-sqrt  30549  normlem7tALT  31215  hhsssh  31365  shintcli  31425  chintcli  31427  omlsi  31500  qlaxr3i  31732  lnophm  32115  nmcopex  32125  nmcoplb  32126  nmbdfnlbi  32145  nmcfnex  32149  nmcfnlb  32150  hmopidmch  32249  hmopidmpj  32250  chirred  32491  threehalves  33000  qfld  33388  1fldgenq  33413  nn0archi  33437  ccfldextrr  33837  ccfldsrarelvec  33862  constrextdg2  33940  constrext2chnlem  33941  constrcon  33965  2sqr3minply  33971  2sqr3nconstr  33972  cos9thpiminplylem6  33978  cos9thpiminply  33979  cos9thpinconstrlem2  33981  trisecnconstr  33983  xrge0iifiso  34126  xrge0iifmhm  34130  xrge0pluscn  34131  rezh  34160  qqh0  34175  qqh1  34176  qqhcn  34182  qqhucn  34183  rerrext  34200  cnrrext  34201  mbfmvolf  34457  hgt750lem  34842  r1filimi  35291  r1filim  35292  r1omfi  35293  r1omhf  35294  r1omfv  35298  subfacval3  35424  erdszelem5  35430  erdszelem8  35433  filnetlem3  36615  filnetlem4  36616  bj-genr  36925  bj-genl  36926  bj-genan  36927  bj-rveccmod  37669  reheibor  38213  cossssid  38931  eqvrelcoss3  39076  3lexlogpow5ineq5  42552  aks6d1c7lem1  42672  tan3rdpi  42836  sin2t3rdpi  42837  sin4t3rdpi  42839  asin1half  42841  fourierdlem68  46624  fourierdlem77  46633  fourierdlem80  46636  fouriersw  46681  etransclem23  46707  gsumge0cl  46821  nthrucw  47338  abcdta  47395  abcdtb  47396  abcdtc  47397  nabctnabc  47401  ppivalnn4  48112  zlmodzxzsubm  48857  zlmodzxzldeplem3  49000  ldepsnlinclem1  49003  ldepsnlinclem2  49004  ldepsnlinc  49006  sepfsepc  49425  prstcleval  50052  prstcocval  50054  setc1onsubc  50099  empty-surprise  50279  amgmwlem  50299  amgmlemALT  50300