ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  simprr Unicode 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  6415  enq0tr  6417  distrnq0  6442  prarloclem3  6480  genplt2i  6493  addlocpr  6519  prmuloc  6547  distrlem1prl  6558  distrlem1pru  6559  ltexprlemopl  6575  ltexprlemopu  6577  ltexprlemfl  6583  ltexprlemrl  6584  ltexprlemfu  6585  ltexprlemru  6586  addcanprleml  6588  addcanprlemu  6589  ltaprg  6592  addextpr  6593  recexprlemdisj  6602  recexprlemloc  6603  aptiprleml  6611  aptiprlemu  6612  ltmprr  6614  archpr  6615  cauappcvgprlemopl  6618  cauappcvgprlemopu  6620  cauappcvgprlemdisj  6623  cauappcvgprlemloc  6624  cauappcvgprlem1  6631  cauappcvgprlemlim  6633  caucvgprlemnkj  6637  caucvgprlemopl  6640  caucvgprlemopu  6642  caucvgprlemdisj  6645  caucvgprlemloc  6646  recexgt0sr  6701  mulgt0sr  6704  addcnsr  6731  mulcnsr  6732  mulcnsrec  6740  axmulcom  6755  axarch  6773  lelttr  6903  ltletr  6904  addcan  6988  addcan2  6989  addsub4  7050  ltadd2  7212  le2add  7234  lt2add  7235  lt2sub  7250  le2sub  7251  rereim  7370  apreap  7371  apreim  7387  mulreim  7388  apcotr  7391  apadd1  7392  addext  7394  apneg  7395  mulext1  7396  mulext  7398  ltleap  7413  mulap0  7417  mulcanapd  7424  rec11ap  7468  rec11rap  7469  divdivdivap  7471  ddcanap  7484  divadddivap  7485  prodgt0gt0  7598  prodgt0  7599  prodge0  7601  lemulge11  7613  lt2mul2div  7626  ltrec  7630  lerec  7631  lerec2  7636  ledivp1  7650  nn0ge0div  8103  qapne  8350  xrlelttr  8492  xrltletr  8493  xrre3  8505  xrrege0  8508  fzass4  8695  fzrev  8716  elfz1b  8722  eluzgtdifelfzo  8823  fzocatel  8825  frec2uzisod  8874  iseqovex  8899  iseqval  8900  expnegzap  8943  ltexp2a  8960  le2sq2  8982  bernneq  9022  expnlbnd2  9027  sqrtsq  9214
  Copyright terms: Public domain W3C validator