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

Theorem simprr 484
Description: Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)
Assertion
Ref Expression
simprr ((φ (ψ χ)) → χ)

Proof of Theorem simprr
StepHypRef Expression
1 id 19 . 2 (χχ)
21ad2antll 460 1 ((φ (ψ χ)) → χ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem is referenced by:  simp1rr  969  simp2rr  973  simp3rr  977  fvmptt  5205  fcof1  5366  fliftfun  5379  isotr  5399  riotass2  5437  acexmidlemab  5449  ovmpt2df  5574  grprinvlem  5637  1stconst  5784  2ndconst  5785  cnvf1olem  5787  smoiso  5858  swoer  6070  erinxp  6116  ecopovsymg  6141  th3qlem1  6144  f1imaen2g  6209  dfplpq2  6338  dfmpq2  6339  mulpipqqs  6357  distrnqg  6371  enq0sym  6414  enq0tr  6416  distrnq0  6441  prarloclem3  6479  genplt2i  6492  addlocpr  6518  prmuloc  6546  distrlem1prl  6557  distrlem1pru  6558  ltexprlemopl  6574  ltexprlemopu  6576  ltexprlemfl  6582  ltexprlemrl  6583  ltexprlemfu  6584  ltexprlemru  6585  addcanprleml  6587  addcanprlemu  6588  ltaprg  6591  addextpr  6592  recexprlemdisj  6601  recexprlemloc  6602  aptiprleml  6610  aptiprlemu  6611  ltmprr  6613  archpr  6614  cauappcvgprlemopl  6617  cauappcvgprlemopu  6619  cauappcvgprlemdisj  6622  cauappcvgprlemloc  6623  cauappcvgprlem1  6630  cauappcvgprlemlim  6632  recexgt0sr  6681  mulgt0sr  6684  addcnsr  6711  mulcnsr  6712  mulcnsrec  6720  axmulcom  6735  axarch  6753  lelttr  6883  ltletr  6884  addcan  6968  addcan2  6969  addsub4  7030  ltadd2  7192  le2add  7214  lt2add  7215  lt2sub  7230  le2sub  7231  rereim  7350  apreap  7351  apreim  7367  mulreim  7368  apcotr  7371  apadd1  7372  addext  7374  apneg  7375  mulext1  7376  mulext  7378  ltleap  7393  mulap0  7397  mulcanapd  7404  rec11ap  7448  rec11rap  7449  divdivdivap  7451  ddcanap  7464  divadddivap  7465  prodgt0gt0  7578  prodgt0  7579  prodge0  7581  lemulge11  7593  lt2mul2div  7606  ltrec  7610  lerec  7611  lerec2  7616  ledivp1  7630  nn0ge0div  8083  qapne  8330  xrlelttr  8472  xrltletr  8473  xrre3  8485  xrrege0  8488  fzass4  8675  fzrev  8696  elfz1b  8702  eluzgtdifelfzo  8803  fzocatel  8805  frec2uzisod  8854  iseqovex  8879  iseqval  8880  expnegzap  8923  ltexp2a  8940  le2sq2  8962  bernneq  9002  expnlbnd2  9007  sqrtsq  9194
  Copyright terms: Public domain W3C validator