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

Theorem simprl 520
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 481 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  simp1rl  1046  simp2rl  1050  simp3rl  1054  rmob  3001  disjiun  3924  reg3exmidlemwe  4493  0xp  4619  imainss  4954  fvmptt  5512  fcof1o  5690  isotr  5717  riota5f  5754  ovmpodf  5902  grprinvlem  5965  grpridd  5967  unielxp  6072  fnmpoovd  6112  1stconst  6118  2ndconst  6119  cnvf1olem  6121  tfrlemi14d  6230  tfrexlem  6231  tfr1onlemres  6246  tfrcllemres  6259  tfrcldm  6260  frecabcl  6296  nnaordi  6404  swoer  6457  qliftfun  6511  ecopovsymg  6528  th3qlem1  6531  mapen  6740  mapxpen  6742  fidifsnen  6764  fisbth  6777  findcard2d  6785  findcard2sd  6786  diffisn  6787  diffifi  6788  ac6sfi  6792  fimax2gtri  6795  fientri3  6803  nnwetri  6804  unsnfi  6807  unsnfidcex  6808  unsnfidcel  6809  fisseneq  6820  fidcenumlemrk  6842  fidcenumlemr  6843  isbth  6855  ordiso2  6920  difinfsnlem  6984  difinfinf  6986  ctmlemr  6993  ctssdccl  6996  fodjum  7018  fodju0  7019  exmidfodomrlemrALT  7059  cc1  7080  cc2lem  7081  cc3  7083  cc4f  7084  cc4n  7086  dfplpq2  7169  dfmpq2  7170  mulpipqqs  7188  distrnqg  7202  ltexnqq  7223  subhalfnqq  7229  distrnq0  7274  prarloclemup  7310  prarloclem3  7312  prarloc  7318  genplt2i  7325  nqprl  7366  nqpru  7367  prmuloc  7381  mullocpr  7386  distrlem4prl  7399  distrlem4pru  7400  ltaddpr  7412  ltexprlemopl  7416  ltexprlemlol  7417  ltexprlemopu  7418  ltexprlemupu  7419  ltexprlemrl  7425  ltexprlemru  7427  addcanprleml  7429  addcanprlemu  7430  ltaprlem  7433  ltaprg  7434  prplnqu  7435  addextpr  7436  recexprlemdisj  7445  recexprlemloc  7446  recexprlem1ssl  7448  aptiprleml  7454  aptiprlemu  7455  ltmprr  7457  archpr  7458  cauappcvgprlemopl  7461  cauappcvgprlemopu  7463  cauappcvgprlemdisj  7466  cauappcvgprlemloc  7467  cauappcvgprlem1  7474  cauappcvgprlem2  7475  cauappcvgprlemlim  7476  caucvgprlemnkj  7481  caucvgprlemopl  7484  caucvgprlemopu  7486  caucvgprlemdisj  7489  caucvgprlemloc  7490  caucvgprlem2  7495  caucvgprprlemnkltj  7504  caucvgprprlemnkeqj  7505  caucvgprprlemnjltk  7506  caucvgprprlemmu  7510  caucvgprprlemopl  7512  caucvgprprlemopu  7514  caucvgprprlemdisj  7517  caucvgprprlemloc  7518  caucvgprprlemexbt  7521  caucvgprprlemaddq  7523  caucvgprprlem2  7525  suplocexprlemrl  7532  suplocexprlemmu  7533  suplocexprlemru  7534  suplocexprlemdisj  7535  suplocexprlemloc  7536  suplocexprlemex  7537  suplocexprlemub  7538  suplocexprlemlub  7539  recexgt0sr  7588  mulgt0sr  7593  prsrriota  7603  caucvgsrlemoffres  7615  suplocsrlem  7623  cnm  7647  addcnsr  7649  mulcnsr  7650  mulcnsrec  7658  axaddcl  7679  axmulcl  7681  axmulcom  7686  rereceu  7704  recriota  7705  axcaucvglemres  7714  axpre-suploclemres  7716  lelttr  7859  ltletr  7860  readdcan  7909  addcan  7949  addcan2  7950  addsub4  8012  ltadd2  8188  le2add  8213  lt2add  8214  lt2sub  8229  le2sub  8230  eqord1  8252  rimul  8354  rereim  8355  ltmul1  8361  apreim  8372  mulreim  8373  apcotr  8376  apadd1  8377  addext  8379  apneg  8380  mulext1  8381  mulext  8383  ltleap  8401  aprcl  8415  mulap0  8422  mulcanapd  8429  receuap  8437  rec11ap  8477  rec11rap  8478  divdivdivap  8480  ddcanap  8493  divadddivap  8494  conjmulap  8496  subrecap  8605  prodgt0gt0  8616  prodge0  8619  ltmul12a  8625  lemulge11  8631  lt2mul2div  8644  ltrec  8648  lerec  8649  lt2msq  8651  lerec2  8654  le2msq  8666  msq11  8667  ledivp1  8668  mulle0r  8709  suprzclex  9156  peano5uzti  9166  supinfneg  9397  infsupneg  9398  qapne  9438  xrlelttr  9596  xrltletr  9597  xrre  9610  xaddge0  9668  xle2add  9669  xlt2add  9670  divelunit  9792  fzass4  9849  fzocatel  9983  exbtwnzlemex  10034  rebtwn2z  10039  qbtwnre  10041  modqid  10129  modqcyc  10139  modqaddabs  10142  modqaddmod  10143  mulqaddmodid  10144  modqadd2mod  10154  modqltm1p1mod  10156  modqsubmod  10162  modqsubmodmod  10163  modqmulmod  10169  modqmulmodr  10170  modqaddmulmod  10171  modqsubdir  10173  frec2uzisod  10187  iseqovex  10236  seqvalcd  10239  seqf  10241  seqovcd  10243  seq3fveq2  10249  seq3shft2  10253  monoord  10256  seq3split  10259  iseqf1olemnab  10268  seq3id2  10289  seq3distr  10293  expcl2lemap  10312  expnegzap  10334  ltexp2a  10352  le2sq2  10375  nn0opth2  10477  bcval5  10516  hashcl  10534  hashen  10537  fihashdom  10556  hashunlem  10557  hashun  10558  fimaxq  10580  zfz1isolem1  10590  zfz1iso  10591  cvg1nlemres  10764  cvg1n  10765  recvguniq  10774  resqrexlemp1rp  10785  resqrexlemoverl  10800  resqrexlemglsq  10801  resqrexlemex  10804  sqrtmul  10814  sqrtsq  10823  absexpzap  10859  absle  10868  abs3lem  10890  amgm2  10897  maxleastlt  10994  maxltsup  10997  fimaxre2  11005  xrmaxleastlt  11032  xrmaxltsup  11034  xrmaxaddlem  11036  climcn2  11085  addcn2  11086  mulcn2  11088  reccn2ap  11089  climcau  11123  summodclem2  11158  summodc  11159  fsumf1o  11166  fisumss  11168  fsum3cvg3  11172  fsumcl2lem  11174  fsumadd  11182  fsum2dlemstep  11210  mptfzshft  11218  fsumrev  11219  fsummulc2  11224  modfsummod  11234  fsumrelem  11247  binom  11260  cvgratnn  11307  mertenslemub  11310  prodmodc  11354  efcllem  11372  tanaddaplem  11452  dvdsval2  11503  moddvds  11509  dvdsabseq  11552  dvdsflip  11556  oexpneg  11581  fldivndvdslt  11639  zsupcllemstep  11645  zssinfcl  11648  bezoutlemnewy  11691  bezoutlemstep  11692  bezoutlemeu  11702  dfgcd3  11705  bezout  11706  dvdsmulgcd  11720  bezoutr  11727  ialgrlem1st  11730  lcmgcdlem  11765  coprmdvds2  11781  qredeu  11785  rpdvds  11787  isprm6  11832  pw2dvdslemn  11850  nonsq  11892  crth  11907  ennnfonelemg  11923  ennnfonelemex  11934  ennnfonelemrnh  11936  ennnfonelemrn  11939  ennnfonelemdm  11940  ennnfonelemnn0  11942  ennnfonelemim  11944  ennnfone  11945  ctinfomlemom  11947  ctinf  11950  ctiunctlemfo  11959  isstruct2r  11980  setscom  12009  epttop  12269  topssnei  12341  restbasg  12347  restopnb  12360  cnfval  12373  cnpfval  12374  iscnp4  12397  cnpnei  12398  cnptopco  12401  cncnp  12409  cnrest2  12415  cnptoprest  12418  cnptoprest2  12419  lmss  12425  lmtopcnp  12429  neitx  12447  txcnp  12450  txrest  12455  txdis  12456  txlm  12458  cnmpt21  12470  imasnopn  12478  xmetres2  12558  blvalps  12567  blval  12568  bl2in  12582  blhalf  12587  blssps  12606  blss  12607  blssexps  12608  blssex  12609  ssblex  12610  blin2  12611  metss2lem  12676  bdmetval  12679  bdmopn  12683  metrest  12685  xmetxp  12686  xmetxpbl  12687  xmettx  12689  metcnp3  12690  txmetcnp  12697  addcncntoplem  12730  elcncf2  12740  mulc1cncf  12755  cncfco  12757  cncfmet  12758  mulcncf  12770  dedekindeulemub  12775  dedekindeulemloc  12776  dedekindeulemlu  12778  dedekindeu  12780  suplociccex  12782  dedekindicclemub  12784  dedekindicclemloc  12785  dedekindicclemlu  12787  dedekindicc  12790  ivthinclemlopn  12793  ivthinclemuopn  12795  ivthdec  12801  limcimolemlt  12812  limcimo  12813  cnplimccntop  12818  limccnp2lem  12824  limccnp2cntop  12825  dvfvalap  12829  dveflem  12865  sin0pilem2  12873  pilem3  12874  ptolemy  12915  ioocosf1o  12945  nnti  13205  pwtrufal  13206  pwf1oexmid  13208  qdencn  13236  cvgcmp2n  13242  trilpolemlt1  13248  supfz  13251  inffz  13252
  Copyright terms: Public domain W3C validator