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  8405  rdgdmlim  8426  oeoa  8607  oeoe  8609  ordtypelem3  9515  ordtypelem5  9517  ordtypelem6  9518  ordtypelem7  9519  ordtypelem9  9521  alephsuc2  10160  negiso  12298  infrenegsup  12301  om2uzoi  14099  faclbnd4lem1  14438  hashunlei  14571  hashsslei  14572  hashle2pr  14623  cos01bnd  16355  cos1bnd  16356  cos2bnd  16357  sincos2sgn  16363  sin4lt0  16364  egt2lt3  16375  divalglem9  16572  bitsinv  16619  drngui  20987  srasca  21456  cnfldfunALT  21694  redvr  21924  refld  21926  iccpnfcnv  25266  xrhmph  25269  recvs  25468  qcvs  25469  i1f1  26012  itg11  26013  dvcos  26304  sinpi  26783  sinhalfpilem  26793  coshalfpi  26799  sincosq1lem  26827  tangtx  26835  sincos4thpi  26843  tan4thpi  26844  sincos6thpi  26845  sincos3rdpi  26846  pige3ALT  26849  logltb  26929  1cubrlem  27170  1cubr  27171  log2tlbnd  27274  cxploglim2  27307  emcllem6  27329  emcllem7  27330  ppiublem1  27530  ppiublem2  27531  bposlem9  27620  lgsdir2lem4  27656  lgsdir2lem5  27657  chebbnd1lem2  27798  chebbnd1lem3  27799  chebbnd1  27800  dchrvmasumlema  27828  mulog2sumlem2  27863  pntlemb  27925  qdrng  27948  upgrbi  29672  upgr1elem  29691  usgrexmpledg  29844  ntrl2v2e  30760  frgrwopreg2  30921  normlem7tALT  31722  hhsssh  31872  shintcli  31932  chintcli  31934  omlsi  32007  qlaxr3i  32239  lnophm  32622  nmcopex  32632  nmcoplb  32633  nmbdfnlbi  32652  nmcfnex  32656  nmcfnlb  32657  hmopidmch  32756  hmopidmpj  32757  chirred  32998  1fldgenq  33927  zringfrac  34129  esplyind  34250  rrxdim  34289  constrextdg2  34424  constrext2chnlem  34425  2sqr3minply  34455  2sqr3nconstr  34456  cos9thpiminply  34463  cos9thpinconstrlem2  34465  trisecnconstr  34467  xrge0hmph  34607  qqh0  34659  qqh1  34660  rerrext  34684  zrhre  34694  qqhre  34695  mbfmvolf  34941  hgt750lem  35323  subfacval2  36021  erdszelem5  36029  erdszelem6  36030  erdszelem7  36031  erdszelem8  36032  filnetlem3  37243  filnetlem4  37244  bj-genr  37552  bj-genl  37553  bj-genan  37554  3lexlogpow5ineq5  43186  aks4d1p1p7  43200  tan3rdpi  43479  cos2t3rdpi  43481  cos4t3rdpi  43483  acos1half  43485  uun0.1  45836  permaxpow  46075  hfstructhf  46106  hfstructcan  46107  pssnssi  46192  fourierdlem62  47254  fourierdlem68  47260  numtowerdt  47992  abcdtb  48072  abcdtc  48073  abcdtd  48074  nabctnabc  48077  zlmodzxzsubm  49547  zlmodzxzldep  49692  ldepsnlinclem1  49693  ldepsnlinclem2  49694  sepfsepc  50112  idfth  50342  idsubc  50344  prstcleval  50739  prstcocval  50741  setc1onsubc  50786  veroquaddetzerod  51062