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  8434  rdgfun  8454  oeoa  8633  oeoe  8635  ssdomg  9038  ordtypelem4  9558  ordtypelem6  9560  ordtypelem7  9561  r1limg  9808  rankwflemb  9830  r1elssi  9842  infxpenlem  10050  ackbij2  10279  wunom  10757  mulnzcnf  11906  negiso  12245  infrenegsup  12248  hashunlei  14460  hashsslei  14461  cos01bnd  16218  cos1bnd  16219  cos2bnd  16220  sin4lt0  16227  egt2lt3  16238  epos  16239  ene1  16242  divalglem5  16430  bitsf1o  16478  gcdaddmlem  16557  sravsca  21202  zrhpsgnmhm  21619  resubgval  21644  re1r  21648  redvr  21652  refld  21654  rzgrp  21658  txindis  23657  icopnfhmeo  24987  iccpnfcnv  24988  iccpnfhmeo  24989  xrhmeo  24990  cnheiborlem  24999  recvs  25192  recvsOLD  25193  qcvs  25194  rrxcph  25439  volf  25577  i1f1  25738  itg11  25739  dvsin  26034  taylthlem2  26430  taylthlem2OLD  26431  reefgim  26508  pilem3  26511  pigt2lt4  26512  pire  26514  pipos  26516  sinhalfpi  26524  tan4thpi  26570  tan4thpiOLD  26571  sincos3rdpi  26573  pigt3  26574  circgrp  26608  circsubm  26609  1cubrlem  26898  1cubr  26899  jensenlem2  27045  amgmlem  27047  emcllem6  27058  emcllem7  27059  harmonicbnd3  27065  ppiublem1  27260  chtub  27270  bposlem7  27348  lgsdir2lem4  27386  lgsdir2lem5  27387  chebbnd1  27530  mulog2sumlem2  27593  pntpbnd1a  27643  pntpbnd2  27645  pntlemb  27655  pntlemk  27664  qrng0  27679  qrng1  27680  qrngneg  27681  qrngdiv  27682  qabsabv  27687  ex-sqrt  30482  normlem7tALT  31147  hhsssh  31297  shintcli  31357  chintcli  31359  omlsi  31432  qlaxr3i  31664  lnophm  32047  nmcopex  32057  nmcoplb  32058  nmbdfnlbi  32077  nmcfnex  32081  nmcfnlb  32082  hmopidmch  32181  hmopidmpj  32182  chirred  32423  threehalves  32881  1fldgenq  33303  nn0archi  33354  ccfldextrr  33675  ccfldsrarelvec  33695  2sqr3minply  33752  xrge0iifiso  33895  xrge0iifmhm  33899  xrge0pluscn  33900  rezh  33931  qqh0  33946  qqh1  33947  qqhcn  33953  qqhucn  33954  rerrext  33971  cnrrext  33972  mbfmvolf  34247  hgt750lem  34644  subfacval3  35173  erdszelem5  35179  erdszelem8  35182  filnetlem3  36362  filnetlem4  36363  bj-genr  36588  bj-genl  36589  bj-genan  36590  bj-rveccmod  37284  reheibor  37825  cossssid  38448  eqvrelcoss3  38599  3lexlogpow5ineq5  42041  aks6d1c7lem1  42161  tan3rdpi  42364  asin1half  42365  fourierdlem68  46129  fourierdlem77  46138  fourierdlem80  46141  fouriersw  46186  etransclem23  46212  gsumge0cl  46326  abcdta  46874  abcdtb  46875  abcdtc  46876  nabctnabc  46880  zlmodzxzsubm  48203  zlmodzxzldeplem3  48347  ldepsnlinclem1  48350  ldepsnlinclem2  48351  ldepsnlinc  48353  sepfsepc  48723  prstcleval  48868  prstcocval  48871  empty-surprise  49012  amgmwlem  49032  amgmlemALT  49033