Theorem simpli 487

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

Syntax hints:   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  tfr2b  8362  rdgfun  8382  oeoa  8562  oeoe  8564  ssdomg  8977  ordtypelem4  9466  ordtypelem6  9468  ordtypelem7  9469  r1limg  9726  rankwflemb  9748  r1elssi  9760  infxpenlem  9966  ackbij2  10195  wunom  10675  mulnzcnf  11830  negiso  12169  infrenegsup  12172  hashunlei  14435  hashsslei  14436  cos01bnd  16201  cos1bnd  16202  cos2bnd  16203  sin4lt0  16210  egt2lt3  16221  epos  16222  ene1  16225  divalglem5  16414  bitsf1o  16462  gcdaddmlem  16541  sravsca  21228  zrhpsgnmhm  21616  resubgval  21641  re1r  21645  redvr  21649  refld  21651  rzgrp  21655  txindis  23674  icopnfhmeo  24985  iccpnfcnv  24986  iccpnfhmeo  24987  xrhmeo  24988  cnheiborlem  24996  recvs  25188  qcvs  25189  rrxcph  25434  volf  25571  i1f1  25732  itg11  25733  dvsin  26024  taylthlem2  26414  reefgim  26490  pilem3  26493  pigt2lt4  26494  pire  26496  pipos  26500  sinhalfpi  26510  tan4thpi  26556  tan4thpiOLD  26557  sincos3rdpi  26559  pigt3  26560  circgrp  26594  circsubm  26595  1cubrlem  26883  1cubr  26884  jensenlem2  27029  amgmlem  27031  emcllem6  27042  emcllem7  27043  harmonicbnd3  27049  ppiublem1  27243  chtub  27253  bposlem7  27331  lgsdir2lem4  27369  lgsdir2lem5  27370  chebbnd1  27513  mulog2sumlem2  27576  pntpbnd1a  27626  pntpbnd2  27628  pntlemb  27638  pntlemk  27647  qrng0  27662  qrng1  27663  qrngneg  27664  qrngdiv  27665  qabsabv  27670  ex-sqrt  30602  normlem7tALT  31268  hhsssh  31418  shintcli  31478  chintcli  31480  omlsi  31553  qlaxr3i  31785  lnophm  32168  nmcopex  32178  nmcoplb  32179  nmbdfnlbi  32198  nmcfnex  32202  nmcfnlb  32203  hmopidmch  32302  hmopidmpj  32303  chirred  32544  threehalves  33053  qfld  33445  1fldgenq  33470  nn0archi  33494  ccfldextrr  33904  ccfldsrarelvec  33929  constrextdg2  34007  constrext2chnlem  34008  constrcon  34032  2sqr3minply  34038  2sqr3nconstr  34039  cos9thpiminplylem6  34045  cos9thpiminply  34046  cos9thpinconstrlem2  34048  trisecnconstr  34050  xrge0iifiso  34193  xrge0iifmhm  34197  xrge0pluscn  34198  rezh  34227  qqh0  34242  qqh1  34243  qqhcn  34249  qqhucn  34250  rerrext  34267  cnrrext  34268  mbfmvolf  34524  hgt750lem  34909  r1filimi  35363  r1filim  35364  r1omfi  35365  r1omhf  35366  r1omfv  35370  subfacval3  35503  erdszelem5  35509  erdszelem8  35512  filnetlem3  36704  filnetlem4  36705  bj-genr  37014  bj-genl  37015  bj-genan  37016  bj-rveccmod  37758  reheibor  38302  cossssid  39020  eqvrelcoss3  39165  3lexlogpow5ineq5  42641  aks6d1c7lem1  42761  tan3rdpi  42925  sin2t3rdpi  42926  sin4t3rdpi  42928  asin1half  42930  fourierdlem68  46712  fourierdlem77  46721  fourierdlem80  46724  fouriersw  46769  etransclem23  46795  gsumge0cl  46909  nthrucw  47426  abcdta  47483  abcdtb  47484  abcdtc  47485  nabctnabc  47489  ppivalnn4  48200  zlmodzxzsubm  48945  zlmodzxzldeplem3  49088  ldepsnlinclem1  49091  ldepsnlinclem2  49092  ldepsnlinc  49094  sepfsepc  49513  prstcleval  50140  prstcocval  50142  setc1onsubc  50187  empty-surprise  50367  amgmwlem  50387  amgmlemALT  50388