ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  simpr Structured version   GIF version

Theorem simpr 103
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 ((φ ψ) → ψ)

Proof of Theorem simpr
StepHypRef Expression
1 ax-ia2 100 1 ((φ ψ) → ψ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
This theorem was proved from axioms:  ax-ia2 100
This theorem is referenced by:  simpri  106  simprd  107  imp  115  adantld  263  ibar  285  pm3.42  315  pm3.4  316  prth  326  sylancom  399  adantll  448  adantrl  450  adantlll  452  adantlrl  454  adantrll  456  adantrrl  458  simpllr  474  simplrr  476  simprlr  478  simprrr  480  anabs7  495  jcab  522  pm4.38  525  pm5.21  598  ioran  656  pm3.14  657  orabsOLD  715  ordi  717  pm4.39  723  pm5.16  725  intnan  826  intnand  828  bimsc1  858  niabn  862  simp1r  917  simp2r  919  simp3r  921  3anandirs  1223  truanOLD  1246  19.26  1350  exsimpr  1491  19.40  1504  cbvexh  1620  cbvexdh  1783  euan  1938  moan  1951  datisi  1992  fresison  2000  rexex  2346  r19.26  2419  r19.40  2442  cbvraldva2  2515  cbvrexdva2  2516  gencbvex  2577  rspct  2626  rspcimdv  2634  rspcimedv  2635  rr19.28v  2660  elrab3t  2674  reu6  2707  rmob  2827  csbiebt  2863  rabssab  3004  difrab  3188  preqsn  3520  opprc2  3546  dfnfc2  3572  intmin4  3617  sndisj  3734  exss  3937  euotd  3965  suctrALT  4107  tfisi  4237  relop  4413  releldm  4496  relelrn  4497  resiexg  4580  trin2  4643  unielrel  4772  relcoi2  4775  iota2df  4818  iota2  4820  funopab4  4863  fun11uni  4895  fneq12  4918  f1ssr  5023  ssimaex  5159  fvmpt2d  5182  fvmptdf  5183  dffo3  5239  ffvresb  5253  fmptco  5255  f1imass  5338  fliftf  5364  fliftval  5365  riota2df  5412  riota5f  5416  ovprc2  5465  eloprabga  5514  eqfnov2  5531  ovmpt2dxf  5549  offval2  5649  ofrfval2  5650  2ndrn  5732  1st2ndbr  5733  cnvf1o  5769  f1o2ndf1  5772  mpt2xopoveq  5777  sprmpt2  5779  dftpos4  5800  tpostpos  5801  tposf12  5806  dfsmo2  5824  smores  5829  tfrlem1  5845  tfrlem3ag  5846  tfrlem3a  5847  tfrlemisucaccv  5860  tfrlemi1  5867  tfrexlem  5870  ersymb  6031  ertr  6032  erref  6037  iserd  6043  swoer  6045  erth  6061  iinerm  6089  erinxp  6091  ecinxp  6092  qsel  6094  qliftel  6097  qliftfun  6099  mulcanenq  6244  ltexnqq  6266  mulcanenq0ec  6300  genpmu  6373  addnqprllem  6382  addnqprulem  6383  addnqprl  6384  addnqpru  6385  nqprloc  6400  appdivnq  6407  appdiv0nq  6408  mulnqprl  6412  mulnqpru  6413  distrlem1prl  6421  distrlem1pru  6422  ltprordil  6428  1idprl  6429  1idpru  6430  ltexprlemrl  6447  ltexprlemru  6449  ltexpri  6450  addcanprleml  6451  addcanprlemu  6452  recexprlem1ssl  6467  recexpr  6472  addsrmo  6490  mulsrmo  6491  addsrpr  6492  mulsrpr  6493  0idsr  6514  1idsr  6515  recexsrlem  6520  addgt0sr  6521  cnegexlem1  6773  cnegex  6776  negeu  6789  pncan  6804  pncan3  6806  npcan  6807  mulneg1  6978
  Copyright terms: Public domain W3C validator