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-1 5  ax-2 6  ax-3 7  ax-mp 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  2596  rexex  2673  r19.26  2746  r19.40  2762  cbvraldva2  2839  cbvrexdva2  2840  gencbvex  2901  rspct  2948  rspcimdv  2956  rr19.28v  2981  reu6  3025  rmob  3134  csbiebt  3172  rabssab  3352  difrab  3529  dfnfc2  3909  intmin4  3955  iota2df  4365  iota2  4367  0nelsuc  4400  nndisjeq  4429  ltfinp1  4462  lenltfin  4469  ncfineleq  4477  evenodddisj  4516  nnadjoin  4520  tfinnn  4534  vfintle  4546  vfinspsslem1  4550  dfphi2  4569  phi11lem1  4595  ideqg  4868  imassrn  5009  xpcan  5057  funopab4  5141  fun11uni  5162  fvelrn  5413  dffo3  5422  ffvresb  5431  eqfnov2  5590  weds  5938  ersymb  5953  erref  5959  elnc  6125  eqncg  6126  ncdisjun  6136  peano4nc  6150  eqtc  6161  leconnnc  6218  taddc  6229  lemuc1  6253  addccan2nc  6265  nchoicelem6  6294  nchoicelem8  6296  nchoicelem17  6305  fnfrec  6320