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

Theorem simprr 492
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 468 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  simp1rr  981  simp2rr  985  simp3rr  989  reg2exmidlema  4287  reg3exmidlemwe  4331  fvmptt  5290  fcof1  5451  fliftfun  5464  isotr  5484  riotass2  5522  acexmidlemab  5534  ovmpt2df  5660  grprinvlem  5723  1stconst  5870  2ndconst  5871  cnvf1olem  5873  f1od2  5884  smoiso  5948  swoer  6165  erinxp  6211  ecopovsymg  6236  th3qlem1  6239  f1imaen2g  6304  fidifsnen  6362  fiunsnnn  6369  fisbth  6371  findcard2d  6379  findcard2sd  6380  diffifi  6382  ac6sfi  6383  nnwetri  6385  supmaxti  6408  ordiso2  6415  dfplpq2  6510  dfmpq2  6511  mulpipqqs  6529  distrnqg  6543  enq0sym  6588  enq0tr  6590  distrnq0  6615  prarloclem3  6653  genplt2i  6666  addlocpr  6692  prmuloc  6722  distrlem1prl  6738  distrlem1pru  6739  ltexprlemopl  6757  ltexprlemopu  6759  ltexprlemfl  6765  ltexprlemrl  6766  ltexprlemfu  6767  ltexprlemru  6768  addcanprleml  6770  addcanprlemu  6771  ltaprg  6775  prplnqu  6776  addextpr  6777  recexprlemdisj  6786  recexprlemloc  6787  aptiprleml  6795  aptiprlemu  6796  ltmprr  6798  archpr  6799  cauappcvgprlemopl  6802  cauappcvgprlemopu  6804  cauappcvgprlemdisj  6807  cauappcvgprlemloc  6808  cauappcvgprlem1  6815  cauappcvgprlemlim  6817  caucvgprlemnkj  6822  caucvgprlemopl  6825  caucvgprlemopu  6827  caucvgprlemdisj  6830  caucvgprlemloc  6831  caucvgprprlemnkltj  6845  caucvgprprlemnkeqj  6846  caucvgprprlemnjltk  6847  caucvgprprlemml  6850  caucvgprprlemmu  6851  caucvgprprlemopl  6853  caucvgprprlemopu  6855  caucvgprprlemdisj  6858  caucvgprprlemloc  6859  caucvgprprlemaddq  6864  recexgt0sr  6916  mulgt0sr  6920  prsrriota  6930  addcnsr  6968  mulcnsr  6969  mulcnsrec  6977  axmulcom  7003  rereceu  7021  axarch  7023  axcaucvglemres  7031  lelttr  7165  ltletr  7166  addcan  7254  addcan2  7255  addsub4  7317  ltadd2  7488  le2add  7513  lt2add  7514  lt2sub  7529  le2sub  7530  rereim  7651  apreap  7652  apreim  7668  mulreim  7669  apcotr  7672  apadd1  7673  addext  7675  apneg  7676  mulext1  7677  mulext  7679  ltleap  7695  mulap0  7709  mulcanapd  7716  rec11ap  7761  rec11rap  7762  divdivdivap  7764  ddcanap  7777  divadddivap  7778  prodgt0gt0  7892  prodgt0  7893  prodge0  7895  lemulge11  7907  lt2mul2div  7920  ltrec  7924  lerec  7925  lerec2  7930  ledivp1  7944  mulle0r  7985  nn0ge0div  8385  qapne  8671  xrlelttr  8823  xrltletr  8824  xrre3  8836  xrrege0  8839  fzass4  9027  fzrev  9048  elfz1b  9054  eluzgtdifelfzo  9155  fzocatel  9157  qbtwnzlemex  9207  rebtwn2z  9211  modqid  9299  modqcyc  9309  modqaddabs  9312  modqaddmod  9313  mulqaddmodid  9314  modqadd2mod  9324  modqltm1p1mod  9326  modqsubmod  9332  modqsubmodmod  9333  modaddmodup  9337  modqmulmod  9339  modqmulmodr  9340  modqaddmulmod  9341  modqsubdir  9343  frec2uzisod  9357  iseqovex  9383  iseqval  9384  iseqshft2  9396  monoord  9399  iseqdistr  9414  expnegzap  9454  ltexp2a  9472  le2sq2  9495  bernneq  9537  expnlbnd2  9542  nn0opth2  9592  faclbnd  9609  ibcval5  9631  cvg1nlemres  9812  cvg1n  9813  resqrexlemp1rp  9833  resqrexlemoverl  9848  resqrexlemex  9852  sqrtsq  9871  abslt  9915  absle  9916  abs3lem  9938  2clim  10053  climcn2  10061  addcn2  10062  mulcn2  10064  climge0  10076  climcau  10097  moddvds  10117  dvdsflip  10163  oexpneg  10188  nn0o  10219  fldivndvdslt  10247  oddpwdclemdc  10261  qdencn  10511
  Copyright terms: Public domain W3C validator