Theorem simpr 447

Description: Elimination of a conjunct. Theorem *3.27 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Nov-2012.)

Assertion

Ref	Expression
simpr	|- ((ph /\ ps) -> ps)

Proof of Theorem simpr

Step	Hyp	Ref	Expression
1		idd 21	. 2 |- (ph -> (ps -> ps))
2	1	imp 418	1 |- ((ph /\ ps) -> ps)

Syntax hints:   -> wi 4   /\ wa 358

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 177  df-an 360

This theorem is referenced by:  simpri  448  adantld  453  ibar  490  pm3.42  543  pm3.4  544  prth  554  sylancom  648  adantll  694  adantrl  696  adantlll  698  adantlrl  700  adantrll  702  adantrrl  704  simpllr  735  simplrr  737  simprlr  739  simprrr  741  anabs7  785  jcab  833  pm4.39  841  pm4.38  842  intnan  880  intnand  882  bimsc1  904  niabn  917  dedlem0b  919  simp1r  980  simp2r  982  simp3r  984  3anandirs  1284  truan  1331  cadan  1392  19.26  1593  19.40  1609  sbft  2025  moan  2255  euan  2261  datisi  2313  fresison  2321  pm2.61da3ne  2597  rexex  2674  r19.26  2747  r19.40  2763  cbvraldva2  2840  cbvrexdva2  2841  gencbvex  2902  rspct  2949  rspcimdv  2957  rr19.28v  2982  reu6  3026  rmob  3135  csbiebt  3173  rabssab  3353  difrab  3530  dfnfc2  3910  intmin4  3956  iota2df  4366  iota2  4368  0nelsuc  4401  nndisjeq  4430  ltfinp1  4463  lenltfin  4470  ncfineleq  4478  evenodddisj  4517  nnadjoin  4521  tfinnn  4535  vfintle  4547  vfinspsslem1  4551  dfphi2  4570  phi11lem1  4596  ideqg  4869  imassrn  5010  xpcan  5058  funopab4  5142  fun11uni  5163  fvelrn  5414  dffo3  5423  ffvresb  5432  eqfnov2  5591  weds  5939  ersymb  5954  erref  5960  elnc  6126  eqncg  6127  ncdisjun  6137  peano4nc  6151  eqtc  6162  leconnnc  6219  taddc  6230  lemuc1  6254  addccan2nc  6266  nchoicelem6  6295  nchoicelem8  6297  nchoicelem17  6306  fnfrec  6321