Theorem simpri 491

Description: Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.)

Hypothesis

Ref	Expression
simpri.1	⊢ (𝜑 ∧ 𝜓)

Assertion

Ref	Expression
simpri	⊢ 𝜓

Proof of Theorem simpri

Step	Hyp	Ref	Expression
1		simpri.1	. 2 ⊢ (𝜑 ∧ 𝜓)
2		simpr 490	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
3	1, 2	ax-mp 5	1 ⊢ 𝜓

This proof depends on syntax axioms:   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  tfr2b  8382  rdgdmlim  8403  oeoa  8584  oeoe  8586  ordtypelem3  9492  ordtypelem5  9494  ordtypelem6  9495  ordtypelem7  9496  ordtypelem9  9498  r1fin  9755  r1tr  9758  r1ordg  9760  r1ord3g  9761  r1pwss  9766  r1val1  9768  rankwflemb  9775  r1elwf  9778  rankr1ai  9780  rankdmr1  9783  rankr1ag  9784  rankr1bg  9785  pwwf  9789  unwf  9792  rankr1clem  9802  rankr1c  9803  rankval3b  9809  rankonidlem  9811  onssr1  9816  rankeq0b  9849  alephsuc2  10131  ackbij2  10292  wunom  10777  negiso  12267  infrenegsup  12270  om2uzoi  14067  faclbnd4lem1  14405  hashunlei  14538  hashsslei  14539  hashle2pr  14590  cos01bnd  16322  cos1bnd  16323  cos2bnd  16324  sincos2sgn  16330  sin4lt0  16331  egt2lt3  16342  divalglem9  16539  bitsinv  16586  drngui  20948  srasca  21417  cnfldfunALT  21655  redvr  21885  refld  21887  iccpnfcnv  25227  xrhmph  25230  recvs  25429  qcvs  25430  i1f1  25973  itg11  25974  dvcos  26265  sinpi  26746  sinhalfpilem  26756  coshalfpi  26762  sincosq1lem  26790  tangtx  26798  sincos4thpi  26806  tan4thpi  26807  sincos6thpi  26808  sincos3rdpi  26809  pige3ALT  26812  logltb  26892  1cubrlem  27133  1cubr  27134  log2tlbnd  27237  cxploglim2  27270  emcllem6  27292  emcllem7  27293  ppiublem1  27493  ppiublem2  27494  bposlem9  27583  lgsdir2lem4  27619  lgsdir2lem5  27620  chebbnd1lem2  27761  chebbnd1lem3  27762  chebbnd1  27763  dchrvmasumlema  27791  mulog2sumlem2  27826  pntlemb  27888  qdrng  27911  upgrbi  29605  upgr1elem  29624  usgrexmpledg  29777  ntrl2v2e  30693  frgrwopreg2  30854  normlem7tALT  31655  hhsssh  31805  shintcli  31865  chintcli  31867  omlsi  31940  qlaxr3i  32172  lnophm  32555  nmcopex  32565  nmcoplb  32566  nmbdfnlbi  32585  nmcfnex  32589  nmcfnlb  32590  hmopidmch  32689  hmopidmpj  32690  chirred  32931  1fldgenq  33818  zringfrac  34020  esplyind  34141  rrxdim  34180  constrextdg2  34315  constrext2chnlem  34316  2sqr3minply  34346  2sqr3nconstr  34347  cos9thpiminply  34354  cos9thpinconstrlem2  34356  trisecnconstr  34358  xrge0hmph  34498  qqh0  34550  qqh1  34551  rerrext  34575  zrhre  34585  qqhre  34586  mbfmvolf  34833  hgt750lem  35215  r11  35656  r12  35657  subfacval2  35873  erdszelem5  35881  erdszelem6  35882  erdszelem7  35883  erdszelem8  35884  filnetlem3  37090  filnetlem4  37091  bj-genr  37399  bj-genl  37400  bj-genan  37401  3lexlogpow5ineq5  43030  aks4d1p1p7  43044  tan3rdpi  43331  cos2t3rdpi  43333  cos4t3rdpi  43335  acos1half  43337  uun0.1  45704  permaxpow  45936  pssnssi  46037  fourierdlem62  47100  fourierdlem68  47106  numtowerdt  47838  abcdtb  47918  abcdtc  47919  abcdtd  47920  nabctnabc  47923  zlmodzxzsubm  49393  zlmodzxzldep  49538  ldepsnlinclem1  49539  ldepsnlinclem2  49540  sepfsepc  49958  idfth  50188  idsubc  50190  prstcleval  50585  prstcocval  50587  setc1onsubc  50632  veroquaddetzerod  50908