Theorem simpri 490

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

This proof depends on syntax axioms:   ∧ wa 400

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 401

This theorem is used by:  tfr2b  8381  rdgdmlim  8402  oeoa  8581  oeoe  8583  ordtypelem3  9480  ordtypelem5  9482  ordtypelem6  9483  ordtypelem7  9484  ordtypelem9  9486  r1fin  9743  r1tr  9746  r1ordg  9748  r1ord3g  9749  r1pwss  9754  r1val1  9756  rankwflemb  9763  r1elwf  9766  rankr1ai  9768  rankdmr1  9771  rankr1ag  9772  rankr1bg  9773  pwwf  9777  unwf  9780  rankr1clem  9790  rankr1c  9791  rankval3b  9796  rankonidlem  9798  onssr1  9801  rankeq0b  9830  alephsuc2  10071  ackbij2  10232  wunom  10711  negiso  12201  infrenegsup  12204  om2uzoi  13998  faclbnd4lem1  14336  hashunlei  14469  hashsslei  14470  hashle2pr  14521  cos01bnd  16248  cos1bnd  16249  cos2bnd  16250  sincos2sgn  16256  sin4lt0  16257  egt2lt3  16268  divalglem9  16465  bitsinv  16512  drngui  20844  srasca  21312  cnfldfunALT  21548  redvr  21778  refld  21780  iccpnfcnv  25114  xrhmph  25117  recvs  25316  qcvs  25317  i1f1  25860  itg11  25861  dvcos  26153  sinpi  26629  sinhalfpilem  26639  coshalfpi  26645  sincosq1lem  26673  tangtx  26681  sincos4thpi  26689  tan4thpi  26690  tan4thpiOLD  26691  sincos6thpi  26692  sincos3rdpi  26693  pige3ALT  26696  logltb  26776  1cubrlem  27017  1cubr  27018  log2tlbnd  27121  cxploglim2  27154  emcllem6  27176  emcllem7  27177  ppiublem1  27377  ppiublem2  27378  bposlem9  27467  lgsdir2lem4  27503  lgsdir2lem5  27504  chebbnd1lem2  27645  chebbnd1lem3  27646  chebbnd1  27647  dchrvmasumlema  27675  mulog2sumlem2  27710  pntlemb  27772  qdrng  27795  upgrbi  29454  upgr1elem  29473  usgrexmpledg  29623  ntrl2v2e  30520  frgrwopreg2  30681  normlem7tALT  31482  hhsssh  31632  shintcli  31692  chintcli  31694  omlsi  31767  qlaxr3i  31999  lnophm  32382  nmcopex  32392  nmcoplb  32393  nmbdfnlbi  32412  nmcfnex  32416  nmcfnlb  32417  hmopidmch  32516  hmopidmpj  32517  chirred  32758  1fldgenq  33652  zringfrac  33853  esplyind  33974  rrxdim  34013  constrextdg2  34148  constrext2chnlem  34149  2sqr3minply  34179  2sqr3nconstr  34180  cos9thpiminply  34187  cos9thpinconstrlem2  34189  trisecnconstr  34191  xrge0hmph  34331  qqh0  34383  qqh1  34384  rerrext  34408  zrhre  34418  qqhre  34419  mbfmvolf  34665  hgt750lem  35047  r11  35496  r12  35497  subfacval2  35687  erdszelem5  35695  erdszelem6  35696  erdszelem7  35697  erdszelem8  35698  filnetlem3  36919  filnetlem4  36920  bj-genr  37228  bj-genl  37229  bj-genan  37230  3lexlogpow5ineq5  42855  aks4d1p1p7  42869  tan3rdpi  43141  cos2t3rdpi  43143  cos4t3rdpi  43145  acos1half  43147  uun0.1  45514  permaxpow  45746  pssnssi  45847  fourierdlem62  46910  fourierdlem68  46916  nthrucw  47635  abcdtb  47691  abcdtc  47692  abcdtd  47693  nabctnabc  47696  zlmodzxzsubm  49167  zlmodzxzldep  49312  ldepsnlinclem1  49313  ldepsnlinclem2  49314  sepfsepc  49734  idfth  49964  idsubc  49966  prstcleval  50361  prstcocval  50363  setc1onsubc  50408