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  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  ch )

Proof of Theorem simprr
StepHypRef Expression
1 id 19 . 2  |-  ( ch 
->  ch )
21ad2antll 460 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  ch )
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  970  simp2rr  974  simp3rr  978  reg2exmidlema  4259  reg3exmidlemwe  4303  fvmptt  5262  fcof1  5423  fliftfun  5436  isotr  5456  riotass2  5494  acexmidlemab  5506  ovmpt2df  5632  grprinvlem  5695  1stconst  5842  2ndconst  5843  cnvf1olem  5845  smoiso  5917  swoer  6134  erinxp  6180  ecopovsymg  6205  th3qlem1  6208  f1imaen2g  6273  fidifsnen  6331  fiunsnnn  6338  fisbth  6340  findcard2d  6348  findcard2sd  6349  diffifi  6351  ac6sfi  6352  nnwetri  6354  ordiso2  6357  dfplpq2  6452  dfmpq2  6453  mulpipqqs  6471  distrnqg  6485  enq0sym  6530  enq0tr  6532  distrnq0  6557  prarloclem3  6595  genplt2i  6608  addlocpr  6634  prmuloc  6664  distrlem1prl  6680  distrlem1pru  6681  ltexprlemopl  6699  ltexprlemopu  6701  ltexprlemfl  6707  ltexprlemrl  6708  ltexprlemfu  6709  ltexprlemru  6710  addcanprleml  6712  addcanprlemu  6713  ltaprg  6717  prplnqu  6718  addextpr  6719  recexprlemdisj  6728  recexprlemloc  6729  aptiprleml  6737  aptiprlemu  6738  ltmprr  6740  archpr  6741  cauappcvgprlemopl  6744  cauappcvgprlemopu  6746  cauappcvgprlemdisj  6749  cauappcvgprlemloc  6750  cauappcvgprlem1  6757  cauappcvgprlemlim  6759  caucvgprlemnkj  6764  caucvgprlemopl  6767  caucvgprlemopu  6769  caucvgprlemdisj  6772  caucvgprlemloc  6773  caucvgprprlemnkltj  6787  caucvgprprlemnkeqj  6788  caucvgprprlemnjltk  6789  caucvgprprlemml  6792  caucvgprprlemmu  6793  caucvgprprlemopl  6795  caucvgprprlemopu  6797  caucvgprprlemdisj  6800  caucvgprprlemloc  6801  caucvgprprlemaddq  6806  recexgt0sr  6858  mulgt0sr  6862  prsrriota  6872  addcnsr  6910  mulcnsr  6911  mulcnsrec  6919  axmulcom  6945  rereceu  6963  axarch  6965  axcaucvglemres  6973  lelttr  7106  ltletr  7107  addcan  7191  addcan2  7192  addsub4  7254  ltadd2  7416  le2add  7439  lt2add  7440  lt2sub  7455  le2sub  7456  rereim  7577  apreap  7578  apreim  7594  mulreim  7595  apcotr  7598  apadd1  7599  addext  7601  apneg  7602  mulext1  7603  mulext  7605  ltleap  7621  mulap0  7635  mulcanapd  7642  rec11ap  7686  rec11rap  7687  divdivdivap  7689  ddcanap  7702  divadddivap  7703  prodgt0gt0  7817  prodgt0  7818  prodge0  7820  lemulge11  7832  lt2mul2div  7845  ltrec  7849  lerec  7850  lerec2  7855  ledivp1  7869  nn0ge0div  8327  qapne  8574  xrlelttr  8722  xrltletr  8723  xrre3  8735  xrrege0  8738  fzass4  8925  fzrev  8946  elfz1b  8952  eluzgtdifelfzo  9053  fzocatel  9055  qbtwnzlemex  9105  rebtwn2z  9109  frec2uzisod  9193  iseqovex  9219  iseqval  9220  iseqshft2  9232  monoord  9235  iseqdistr  9249  expnegzap  9289  ltexp2a  9306  le2sq2  9329  bernneq  9369  expnlbnd2  9374  cvg1nlemres  9584  cvg1n  9585  resqrexlemp1rp  9604  resqrexlemoverl  9619  resqrexlemex  9623  sqrtsq  9642  abslt  9684  absle  9685  abs3lem  9707  2clim  9822  climcn2  9830  addcn2  9831  mulcn2  9833  climge0  9845  climcau  9866  qdencn  10123
  Copyright terms: Public domain W3C validator