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

Theorem simprl 491
Description: Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)
Assertion
Ref Expression
simprl  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  ps )

Proof of Theorem simprl
StepHypRef Expression
1 id 19 . 2  |-  ( ps 
->  ps )
21ad2antrl 467 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  ps )
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:  simp1rl  980  simp2rl  984  simp3rl  988  rmob  2877  reg3exmidlemwe  4330  0xp  4447  imainss  4766  fvmptt  5289  fcof1o  5456  isotr  5483  riota5f  5519  ovmpt2df  5659  grprinvlem  5722  grpridd  5724  unielxp  5827  1stconst  5869  2ndconst  5870  cnvf1olem  5872  tfrlemi14d  5977  tfrexlem  5978  nnaordi  6111  swoer  6164  qliftfun  6218  ecopovsymg  6235  th3qlem1  6238  fidifsnen  6361  fisbth  6370  findcard2d  6378  findcard2sd  6379  diffisn  6380  diffifi  6381  ac6sfi  6382  fientri3  6383  nnwetri  6384  ordiso2  6414  dfplpq2  6509  dfmpq2  6510  mulpipqqs  6528  distrnqg  6542  ltexnqq  6563  subhalfnqq  6569  distrnq0  6614  prarloclemup  6650  prarloclem3  6652  prarloc  6658  genplt2i  6665  nqprl  6706  nqpru  6707  prmuloc  6721  mullocpr  6726  distrlem4prl  6739  distrlem4pru  6740  ltaddpr  6752  ltexprlemopl  6756  ltexprlemlol  6757  ltexprlemopu  6758  ltexprlemupu  6759  ltexprlemrl  6765  ltexprlemru  6767  addcanprleml  6769  addcanprlemu  6770  ltaprlem  6773  ltaprg  6774  prplnqu  6775  addextpr  6776  recexprlemdisj  6785  recexprlemloc  6786  recexprlem1ssl  6788  aptiprleml  6794  aptiprlemu  6795  ltmprr  6797  archpr  6798  cauappcvgprlemopl  6801  cauappcvgprlemopu  6803  cauappcvgprlemdisj  6806  cauappcvgprlemloc  6807  cauappcvgprlem1  6814  cauappcvgprlem2  6815  cauappcvgprlemlim  6816  caucvgprlemnkj  6821  caucvgprlemopl  6824  caucvgprlemopu  6826  caucvgprlemdisj  6829  caucvgprlemloc  6830  caucvgprlem2  6835  caucvgprprlemnkltj  6844  caucvgprprlemnkeqj  6845  caucvgprprlemnjltk  6846  caucvgprprlemmu  6850  caucvgprprlemopl  6852  caucvgprprlemopu  6854  caucvgprprlemdisj  6857  caucvgprprlemloc  6858  caucvgprprlemexbt  6861  caucvgprprlemaddq  6863  caucvgprprlem2  6865  recexgt0sr  6915  mulgt0sr  6919  prsrriota  6929  caucvgsrlemoffres  6941  addcnsr  6967  mulcnsr  6968  mulcnsrec  6976  axaddcl  6997  axmulcl  6999  axmulcom  7002  rereceu  7020  recriota  7021  axcaucvglemres  7030  lelttr  7164  ltletr  7165  readdcan  7213  addcan  7253  addcan2  7254  addsub4  7316  ltadd2  7487  le2add  7512  lt2add  7513  lt2sub  7528  le2sub  7529  rimul  7649  rereim  7650  ltmul1  7656  apreim  7667  mulreim  7668  apcotr  7671  apadd1  7672  addext  7674  apneg  7675  mulext1  7676  mulext  7678  ltleap  7694  mulap0  7708  mulcanapd  7715  receuap  7723  rec11ap  7760  rec11rap  7761  divdivdivap  7763  ddcanap  7776  divadddivap  7777  conjmulap  7779  prodgt0gt0  7891  prodge0  7894  ltmul12a  7900  lemulge11  7906  lt2mul2div  7919  ltrec  7923  lerec  7924  lt2msq  7926  lerec2  7929  le2msq  7941  msq11  7942  ledivp1  7943  mulle0r  7984  peano5uzti  8404  qapne  8670  xrlelttr  8822  xrltletr  8823  xrre  8833  divelunit  8970  fzass4  9026  fzocatel  9156  qbtwnzlemex  9206  rebtwn2z  9210  qbtwnre  9212  modqid  9293  modqcyc  9303  modqaddabs  9306  modqaddmod  9307  mulqaddmodid  9308  modqadd2mod  9318  modqltm1p1mod  9320  modqsubmod  9326  modqsubmodmod  9327  modqmulmod  9333  modqmulmodr  9334  modqaddmulmod  9335  modqsubdir  9337  frec2uzisod  9351  iseqovex  9377  iseqval  9378  iseqfveq2  9386  iseqshft2  9390  monoord  9393  iseqsplit  9396  iseqdistr  9408  expivallem  9415  expcl2lemap  9426  expnegzap  9448  ltexp2a  9466  le2sq2  9489  nn0opth2  9585  ibcval5  9624  cvg1nlemres  9805  cvg1n  9806  recvguniq  9814  resqrexlemp1rp  9825  resqrexlemoverl  9840  resqrexlemglsq  9841  resqrexlemex  9844  sqrtmul  9854  sqrtsq  9863  absexpzap  9899  absle  9908  abs3lem  9930  amgm2  9937  climcn2  10053  addcn2  10054  mulcn2  10056  climcau  10089  dvdsval2  10103  moddvds  10109  dvdsabseq  10151  dvdsflip  10155  oexpneg  10180  pw2dvdslemn  10225  ialgrlem1st  10236  qdencn  10483
  Copyright terms: Public domain W3C validator