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

Theorem simprr 499
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 475 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  simp1rr  1009  simp2rr  1013  simp3rr  1017  disjiun  3840  reg2exmidlema  4350  reg3exmidlemwe  4394  fvmptt  5394  fcof1  5562  fliftfun  5575  isotr  5595  riotass2  5634  acexmidlemab  5646  ovmpt2df  5776  grprinvlem  5839  1stconst  5986  2ndconst  5987  cnvf1olem  5989  f1od2  6000  smoiso  6067  tfrcldm  6128  tfrcl  6129  swoer  6320  erinxp  6366  ecopovsymg  6391  th3qlem1  6394  f1imaen2g  6510  mapdom1g  6563  fict  6584  fidifsnen  6586  dif1enen  6596  fiunsnnn  6597  fisbth  6599  findcard2d  6607  findcard2sd  6608  diffifi  6610  ac6sfi  6614  fimax2gtri  6617  nnwetri  6626  unsnfi  6629  unsnfidcex  6630  unsnfidcel  6631  fisseneq  6642  ssfirab  6643  fidcenumlemrk  6663  fidcenumlemr  6664  sbthlemi6  6671  sbthlemi8  6673  isbth  6676  supmaxti  6699  infminti  6722  ordiso2  6728  eldju2ndl  6763  eldju2ndr  6764  fodjuomnilemm  6801  fodjuomnilem0  6802  exmidfodomrlemrALT  6829  dfplpq2  6913  dfmpq2  6914  mulpipqqs  6932  distrnqg  6946  enq0sym  6991  enq0tr  6993  distrnq0  7018  prarloclem3  7056  genplt2i  7069  addlocpr  7095  prmuloc  7125  distrlem1prl  7141  distrlem1pru  7142  ltexprlemopl  7160  ltexprlemopu  7162  ltexprlemfl  7168  ltexprlemrl  7169  ltexprlemfu  7170  ltexprlemru  7171  addcanprleml  7173  addcanprlemu  7174  ltaprg  7178  prplnqu  7179  addextpr  7180  recexprlemdisj  7189  recexprlemloc  7190  aptiprleml  7198  aptiprlemu  7199  ltmprr  7201  archpr  7202  cauappcvgprlemopl  7205  cauappcvgprlemopu  7207  cauappcvgprlemdisj  7210  cauappcvgprlemloc  7211  cauappcvgprlem1  7218  cauappcvgprlemlim  7220  caucvgprlemnkj  7225  caucvgprlemopl  7228  caucvgprlemopu  7230  caucvgprlemdisj  7233  caucvgprlemloc  7234  caucvgprprlemnkltj  7248  caucvgprprlemnkeqj  7249  caucvgprprlemnjltk  7250  caucvgprprlemml  7253  caucvgprprlemmu  7254  caucvgprprlemopl  7256  caucvgprprlemopu  7258  caucvgprprlemdisj  7261  caucvgprprlemloc  7262  caucvgprprlemaddq  7267  recexgt0sr  7319  mulgt0sr  7323  prsrriota  7333  addcnsr  7371  mulcnsr  7372  mulcnsrec  7380  axmulcom  7406  rereceu  7424  axarch  7426  axcaucvglemres  7434  lelttr  7573  ltletr  7574  addcan  7662  addcan2  7663  addsub4  7725  ltadd2  7897  le2add  7922  lt2add  7923  lt2sub  7938  le2sub  7939  eqord1  7961  rereim  8063  apreap  8064  apreim  8080  mulreim  8081  apcotr  8084  apadd1  8085  addext  8087  apneg  8088  mulext1  8089  mulext  8091  ltleap  8107  mulap0  8123  mulcanapd  8130  rec11ap  8177  rec11rap  8178  divdivdivap  8180  ddcanap  8193  divadddivap  8194  prodgt0gt0  8312  prodgt0  8313  prodge0  8315  lemulge11  8327  lt2mul2div  8340  ltrec  8344  lerec  8345  lerec2  8350  ledivp1  8364  mulle0r  8405  nn0ge0div  8833  suprzclex  8844  qapne  9124  xrlelttr  9271  xrltletr  9272  xrre3  9284  xrrege0  9287  fzass4  9476  fzrev  9498  elfz1b  9504  eluzgtdifelfzo  9608  fzocatel  9610  exbtwnzlemex  9661  rebtwn2z  9666  modqid  9756  modqcyc  9766  modqaddabs  9769  modqaddmod  9770  mulqaddmodid  9771  modqadd2mod  9781  modqltm1p1mod  9783  modqsubmod  9789  modqsubmodmod  9790  modaddmodup  9794  modqmulmod  9796  modqmulmodr  9797  modqaddmulmod  9798  modqsubdir  9800  frec2uzisod  9814  iseqovex  9870  iseqval  9871  iseqfclt  9879  seqf  9880  iseqshft2  9898  monoord  9904  iseqf1olemnab  9917  iseqdistr  9945  seq3distr  9946  expnegzap  9989  ltexp2a  10007  le2sq2  10030  bernneq  10074  expnlbnd2  10079  nn0opth2  10132  faclbnd  10149  ibcval5  10171  hashcl  10189  hashen  10192  fihashdom  10211  hashunlem  10212  hashun  10213  hashxp  10234  fimaxq  10235  zfz1isolem1  10245  zfz1iso  10246  iseqcoll  10247  cvg1nlemres  10418  cvg1n  10419  resqrexlemp1rp  10439  resqrexlemoverl  10454  resqrexlemex  10458  sqrtsq  10477  abslt  10521  absle  10522  abs3lem  10544  maxleastlt  10648  maxltsup  10651  fimaxre2  10658  negfi  10659  2clim  10689  climcn2  10698  addcn2  10699  mulcn2  10701  climge0  10713  climcau  10736  isummolem2  10772  isummo  10773  zisum  10774  fsumf1o  10782  fisumss  10784  fsum3cvg3  10789  fsumcl2lem  10792  fsumadd  10800  mptfzshft  10836  fsumrev  10837  fsummulc2  10842  fsumconst  10848  modfsummod  10852  fsumrelem  10865  binom  10878  cvgratnn  10925  mertenslemub  10928  efcllem  10949  tanaddaplem  11029  moddvds  11083  dvdsflip  11130  oexpneg  11155  nn0o  11185  fldivndvdslt  11213  zsupcllemstep  11219  zsupcllemex  11220  zssinfcl  11222  bezoutlemnewy  11263  bezoutlemstep  11264  bezoutlemeu  11274  dfgcd3  11277  dfgcd2  11281  dvdsmulgcd  11292  bezoutr  11299  lcmgcdlem  11337  coprmdvds2  11353  qredeu  11357  rpdvds  11359  cncongr1  11363  prmind2  11380  isprm6  11404  oddpwdclemdc  11429  nonsq  11463  hashdvds  11475  crth  11478  hashgcdlem  11481  hashgcdeq  11482  isstruct2r  11505  setscom  11534  elcncf2  11630  mulc1cncf  11645  cncfco  11647  nnsucpred  11891  nnti  11892  qdencn  11915  supfz  11916  inffz  11917
  Copyright terms: Public domain W3C validator