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

Theorem simprl 483
Description: Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)
Assertion
Ref Expression
simprl

Proof of Theorem simprl
StepHypRef Expression
1 id 19 . 2
21ad2antrl 459 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:  simp1rl  968  simp2rl  972  simp3rl  976  rmob  2844  0xp  4363  imainss  4682  fvmptt  5205  fcof1o  5372  isotr  5399  riota5f  5435  ovmpt2df  5574  grprinvlem  5637  grpridd  5639  unielxp  5742  1stconst  5784  2ndconst  5785  cnvf1olem  5787  tfrlemi14d  5888  tfrexlem  5889  nnaordi  6017  swoer  6070  qliftfun  6124  ecopovsymg  6141  th3qlem1  6144  dfplpq2  6338  dfmpq2  6339  mulpipqqs  6357  distrnqg  6371  ltexnqq  6391  subhalfnqq  6397  distrnq0  6441  prarloclemup  6477  prarloclem3  6479  prarloc  6485  genplt2i  6492  nqprl  6532  prmuloc  6546  mullocpr  6551  distrlem4prl  6559  distrlem4pru  6560  ltaddpr  6570  ltexprlemopl  6574  ltexprlemlol  6575  ltexprlemopu  6576  ltexprlemupu  6577  ltexprlemrl  6583  ltexprlemru  6585  addcanprleml  6587  addcanprlemu  6588  ltaprlem  6590  ltaprg  6591  addextpr  6592  recexprlemdisj  6601  recexprlemloc  6602  recexprlem1ssl  6604  aptiprleml  6610  aptiprlemu  6611  ltmprr  6613  archpr  6614  cauappcvgprlemopl  6617  cauappcvgprlemopu  6619  cauappcvgprlemdisj  6622  cauappcvgprlemloc  6623  cauappcvgprlem1  6630  cauappcvgprlem2  6631  cauappcvgprlemlim  6632  recexgt0sr  6681  mulgt0sr  6684  addcnsr  6711  mulcnsr  6712  mulcnsrec  6720  axaddcl  6730  axmulcl  6732  axmulcom  6735  lelttr  6883  ltletr  6884  readdcan  6930  addcan  6968  addcan2  6969  addsub4  7030  ltadd2  7192  le2add  7214  lt2add  7215  lt2sub  7230  le2sub  7231  rimul  7349  rereim  7350  ltmul1  7356  apreim  7367  mulreim  7368  apcotr  7371  apadd1  7372  addext  7374  apneg  7375  mulext1  7376  mulext  7378  ltleap  7393  mulap0  7397  mulcanapd  7404  receuap  7412  rec11ap  7448  rec11rap  7449  divdivdivap  7451  ddcanap  7464  divadddivap  7465  conjmulap  7467  prodgt0gt0  7578  prodge0  7581  ltmul12a  7587  lemulge11  7593  lt2mul2div  7606  ltrec  7610  lerec  7611  lt2msq  7613  lerec2  7616  le2msq  7628  msq11  7629  ledivp1  7630  peano5uzti  8102  qapne  8330  xrlelttr  8472  xrltletr  8473  xrre  8483  divelunit  8620  fzass4  8675  fzocatel  8805  frec2uzisod  8854  iseqovex  8879  iseqval  8880  iseqfveq2  8885  expivallem  8890  expcl2lemap  8901  expnegzap  8923  ltexp2a  8940  le2sq2  8962  sqrtsq  9194
  Copyright terms: Public domain W3C validator