Theorem simpli 473

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

Syntax hints:   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  exan  1775  exanOLD  1776  pwundif  4935  tfr2b  7357  rdgfun  7377  oeoa  7542  oeoe  7544  ssdomg  7865  ordtypelem4  8287  ordtypelem6  8289  ordtypelem7  8290  r1limg  8495  rankwflemb  8517  r1elssi  8529  infxpenlem  8697  ackbij2  8926  wunom  9399  mulnzcnopr  10525  negiso  10853  infrenegsup  10856  hashunlei  13027  hashsslei  13028  cos01bnd  14704  cos1bnd  14705  cos2bnd  14706  sin4lt0  14713  egt2lt3  14722  epos  14723  ene1  14726  divalglem5  14907  bitsf1o  14954  gcdaddmlem  15032  strlemor1  15745  zrhpsgnmhm  19697  resubgval  19722  re1r  19726  redvr  19730  refld  19732  txindis  21195  icopnfhmeo  22498  iccpnfcnv  22499  iccpnfhmeo  22500  xrhmeo  22501  cnheiborlem  22509  rrxcph  22933  volf  23049  i1f1  23208  itg11  23209  dvsin  23494  taylthlem2  23877  reefgim  23953  pilem3  23956  pigt2lt4  23957  pire  23959  pipos  23961  sinhalfpi  23969  tan4thpi  24015  sincos3rdpi  24017  circgrp  24047  circsubm  24048  rzgrp  24049  1cubrlem  24313  1cubr  24314  jensenlem2  24459  amgmlem  24461  emcllem6  24472  emcllem7  24473  emgt0  24478  harmonicbnd3  24479  ppiublem1  24672  chtub  24682  bposlem7  24760  lgsdir2lem4  24798  lgsdir2lem5  24799  chebbnd1  24906  mulog2sumlem2  24969  pntpbnd1a  25019  pntpbnd2  25021  pntlemb  25031  pntlemk  25040  qrng0  25055  qrng1  25056  qrngneg  25057  qrngdiv  25058  qabsabv  25063  2trllemE  25877  ex-sqrt  26497  normlem7tALT  27154  hhsssh  27304  shintcli  27366  chintcli  27368  omlsi  27441  qlaxr3i  27673  lnophm  28056  nmcopex  28066  nmcoplb  28067  nmbdfnlbi  28086  nmcfnex  28090  nmcfnlb  28091  hmopidmch  28190  hmopidmpj  28191  chirred  28432  nn0archi  28968  xrge0iifiso  29103  xrge0iifmhm  29107  xrge0pluscn  29108  rezh  29137  qqh0  29150  qqh1  29151  qqhcn  29157  qqhucn  29158  rerrext  29175  cnrrext  29176  mbfmvolf  29449  subfacval3  30219  erdszelem5  30225  erdszelem8  30228  filnetlem3  31339  filnetlem4  31340  bj-genr  31570  bj-genl  31571  bj-genan  31572  pigt3  32366  reheibor  32602  fourierdlem68  38861  fourierdlem77  38870  fourierdlem80  38873  fouriersw  38918  etransclem23  38944  gsumge0cl  39058  abcdta  39535  abcdtb  39536  abcdtc  39537  nabctnabc  39541  zlmodzxzsubm  41922  zlmodzxzldeplem3  42077  ldepsnlinclem1  42080  ldepsnlinclem2  42081  ldepsnlinc  42083  empty-surprise  42290  amgmwlem  42310  amgmlemALT  42311