Theorem simpri 485

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

Syntax hints:   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  tfr2b  8324  rdgdmlim  8345  oeoa  8521  oeoe  8523  ordtypelem3  9416  ordtypelem5  9418  ordtypelem6  9419  ordtypelem7  9420  ordtypelem9  9422  r1fin  9676  r1tr  9679  r1ordg  9681  r1ord3g  9682  r1pwss  9687  r1val1  9689  rankwflemb  9696  r1elwf  9699  rankr1ai  9701  rankdmr1  9704  rankr1ag  9705  rankr1bg  9706  pwwf  9710  unwf  9713  rankr1clem  9723  rankr1c  9724  rankval3b  9729  rankonidlem  9731  onssr1  9734  rankeq0b  9763  alephsuc2  9981  ackbij2  10143  wunom  10621  negiso  12112  infrenegsup  12115  om2uzoi  13872  faclbnd4lem1  14210  hashunlei  14342  hashsslei  14343  hashle2pr  14394  cos01bnd  16105  cos1bnd  16106  cos2bnd  16107  sincos2sgn  16113  sin4lt0  16114  egt2lt3  16125  divalglem9  16322  bitsinv  16369  drngui  20660  srasca  21124  cnfldfunALT  21316  cnfldfunALTOLD  21329  redvr  21564  refld  21566  iccpnfcnv  24879  xrhmph  24882  recvs  25083  qcvs  25084  i1f1  25628  itg11  25629  dvcos  25924  sinpi  26402  sinhalfpilem  26409  coshalfpi  26415  sincosq1lem  26443  tangtx  26451  sincos4thpi  26459  tan4thpi  26460  tan4thpiOLD  26461  sincos6thpi  26462  sincos3rdpi  26463  pige3ALT  26466  logltb  26546  1cubrlem  26788  1cubr  26789  log2tlbnd  26892  cxploglim2  26926  emcllem6  26948  emcllem7  26949  ppiublem1  27150  ppiublem2  27151  bposlem9  27240  lgsdir2lem4  27276  lgsdir2lem5  27277  chebbnd1lem2  27418  chebbnd1lem3  27419  chebbnd1  27420  dchrvmasumlema  27448  mulog2sumlem2  27483  pntlemb  27545  qdrng  27568  upgrbi  29082  upgr1elem  29101  usgrexmpledg  29251  ntrl2v2e  30149  frgrwopreg2  30310  normlem7tALT  31110  hhsssh  31260  shintcli  31320  chintcli  31322  omlsi  31395  qlaxr3i  31627  lnophm  32010  nmcopex  32020  nmcoplb  32021  nmbdfnlbi  32040  nmcfnex  32044  nmcfnlb  32045  hmopidmch  32144  hmopidmpj  32145  chirred  32386  1fldgenq  33299  zringfrac  33530  rrxdim  33638  constrextdg2  33773  constrext2chnlem  33774  2sqr3minply  33804  2sqr3nconstr  33805  cos9thpiminply  33812  cos9thpinconstrlem2  33814  trisecnconstr  33816  xrge0hmph  33956  qqh0  34008  qqh1  34009  rerrext  34033  zrhre  34043  qqhre  34044  mbfmvolf  34290  hgt750lem  34675  r11  35116  r12  35117  subfacval2  35242  erdszelem5  35250  erdszelem6  35251  erdszelem7  35252  erdszelem8  35253  filnetlem3  36435  filnetlem4  36436  bj-genr  36661  bj-genl  36662  bj-genan  36663  3lexlogpow5ineq5  42163  aks4d1p1p7  42177  tan3rdpi  42460  cos2t3rdpi  42462  cos4t3rdpi  42464  acos1half  42466  uun0.1  44884  permaxpow  45116  pssnssi  45212  fourierdlem62  46280  fourierdlem68  46286  nthrucw  46998  abcdtb  47040  abcdtc  47041  abcdtd  47042  nabctnabc  47045  zlmodzxzsubm  48473  zlmodzxzldep  48619  ldepsnlinclem1  48620  ldepsnlinclem2  48621  sepfsepc  49042  idfth  49273  idsubc  49275  prstcleval  49670  prstcocval  49672  setc1onsubc  49717