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

This theorem is referenced by:  tfr2b  8398  rdgfun  8418  oeoa  8599  oeoe  8601  ssdomg  8998  ordtypelem4  9518  ordtypelem6  9520  ordtypelem7  9521  r1limg  9768  rankwflemb  9790  r1elssi  9802  infxpenlem  10010  ackbij2  10240  wunom  10717  mulnzcnopr  11864  negiso  12198  infrenegsup  12201  hashunlei  14389  hashsslei  14390  cos01bnd  16133  cos1bnd  16134  cos2bnd  16135  sin4lt0  16142  egt2lt3  16153  epos  16154  ene1  16157  divalglem5  16344  bitsf1o  16390  gcdaddmlem  16469  sravsca  20945  zrhpsgnmhm  21356  resubgval  21381  re1r  21385  redvr  21389  refld  21391  rzgrp  21395  txindis  23358  icopnfhmeo  24683  iccpnfcnv  24684  iccpnfhmeo  24685  xrhmeo  24686  cnheiborlem  24694  recvs  24886  recvsOLD  24887  qcvs  24888  rrxcph  25133  volf  25270  i1f1  25431  itg11  25432  dvsin  25723  taylthlem2  26110  reefgim  26186  pilem3  26189  pigt2lt4  26190  pire  26192  pipos  26194  sinhalfpi  26202  tan4thpi  26248  sincos3rdpi  26250  pigt3  26251  circgrp  26285  circsubm  26286  1cubrlem  26570  1cubr  26571  jensenlem2  26716  amgmlem  26718  emcllem6  26729  emcllem7  26730  harmonicbnd3  26736  ppiublem1  26929  chtub  26939  bposlem7  27017  lgsdir2lem4  27055  lgsdir2lem5  27056  chebbnd1  27199  mulog2sumlem2  27262  pntpbnd1a  27312  pntpbnd2  27314  pntlemb  27324  pntlemk  27333  qrng0  27348  qrng1  27349  qrngneg  27350  qrngdiv  27351  qabsabv  27356  ex-sqrt  29962  normlem7tALT  30627  hhsssh  30777  shintcli  30837  chintcli  30839  omlsi  30912  qlaxr3i  31144  lnophm  31527  nmcopex  31537  nmcoplb  31538  nmbdfnlbi  31557  nmcfnex  31561  nmcfnlb  31562  hmopidmch  31661  hmopidmpj  31662  chirred  31903  threehalves  32336  1fldgenq  32670  nn0archi  32720  ccfldextrr  33003  ccfldsrarelvec  33022  xrge0iifiso  33201  xrge0iifmhm  33205  xrge0pluscn  33206  rezh  33237  qqh0  33250  qqh1  33251  qqhcn  33257  qqhucn  33258  rerrext  33275  cnrrext  33276  mbfmvolf  33551  hgt750lem  33949  subfacval3  34466  erdszelem5  34472  erdszelem8  34475  filnetlem3  35568  filnetlem4  35569  bj-genr  35787  bj-genl  35788  bj-genan  35789  bj-rveccmod  36486  reheibor  37010  cossssid  37640  eqvrelcoss3  37791  3lexlogpow5ineq5  41231  fourierdlem68  45189  fourierdlem77  45198  fourierdlem80  45201  fouriersw  45246  etransclem23  45272  gsumge0cl  45386  abcdta  45934  abcdtb  45935  abcdtc  45936  nabctnabc  45940  zlmodzxzsubm  47124  zlmodzxzldeplem3  47271  ldepsnlinclem1  47274  ldepsnlinclem2  47275  ldepsnlinc  47277  sepfsepc  47648  prstcleval  47776  prstcocval  47779  empty-surprise  47917  amgmwlem  47937  amgmlemALT  47938