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

Theorem simprr 504
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 480 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  ch )
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:  simp1rr  1030  simp2rr  1034  simp3rr  1038  disjiun  3892  reg2exmidlema  4417  reg3exmidlemwe  4461  nnsucpred  4498  fvmptt  5478  fcof1  5650  fliftfun  5663  isotr  5683  riotass2  5722  acexmidlemab  5734  ovmpodf  5868  grprinvlem  5931  fnmpoovd  6078  1stconst  6084  2ndconst  6085  cnvf1olem  6087  f1od2  6098  smoiso  6165  tfrcldm  6226  tfrcl  6227  nntr2  6365  swoer  6423  erinxp  6469  ecopovsymg  6494  th3qlem1  6497  f1imaen2g  6653  mapdom1g  6707  fict  6728  fidifsnen  6730  dif1enen  6740  fiunsnnn  6741  fisbth  6743  findcard2d  6751  findcard2sd  6752  diffifi  6754  ac6sfi  6758  fimax2gtri  6761  nnwetri  6770  unsnfi  6773  unsnfidcex  6774  unsnfidcel  6775  fisseneq  6786  ssfirab  6788  fidcenumlemrk  6808  fidcenumlemr  6809  sbthlemi6  6816  sbthlemi8  6818  isbth  6821  fiuni  6832  supmaxti  6857  infminti  6880  ordiso2  6886  eldju2ndl  6923  eldju2ndr  6924  omp1eomlem  6945  difinfsnlem  6950  difinfinf  6952  ctmlemr  6959  ctssdccl  6962  fodjum  6984  fodju0  6985  exmidfodomrlemrALT  7023  acfun  7027  exmidaclem  7028  ccfunen  7043  dfplpq2  7126  dfmpq2  7127  mulpipqqs  7145  distrnqg  7159  enq0sym  7204  enq0tr  7206  distrnq0  7231  prarloclem3  7269  genplt2i  7282  addlocpr  7308  prmuloc  7338  distrlem1prl  7354  distrlem1pru  7355  ltexprlemopl  7373  ltexprlemopu  7375  ltexprlemfl  7381  ltexprlemrl  7382  ltexprlemfu  7383  ltexprlemru  7384  addcanprleml  7386  addcanprlemu  7387  ltaprg  7391  prplnqu  7392  addextpr  7393  recexprlemdisj  7402  recexprlemloc  7403  aptiprleml  7411  aptiprlemu  7412  ltmprr  7414  archpr  7415  cauappcvgprlemopl  7418  cauappcvgprlemopu  7420  cauappcvgprlemdisj  7423  cauappcvgprlemloc  7424  cauappcvgprlem1  7431  cauappcvgprlemlim  7433  caucvgprlemnkj  7438  caucvgprlemopl  7441  caucvgprlemopu  7443  caucvgprlemdisj  7446  caucvgprlemloc  7447  caucvgprprlemnkltj  7461  caucvgprprlemnkeqj  7462  caucvgprprlemnjltk  7463  caucvgprprlemml  7466  caucvgprprlemmu  7467  caucvgprprlemopl  7469  caucvgprprlemopu  7471  caucvgprprlemdisj  7474  caucvgprprlemloc  7475  caucvgprprlemaddq  7480  suplocexprlemrl  7489  suplocexprlemmu  7490  suplocexprlemru  7491  suplocexprlemdisj  7492  suplocexprlemloc  7493  suplocexprlemex  7494  suplocexprlemub  7495  recexgt0sr  7545  mulgt0sr  7550  prsrriota  7560  suplocsrlem  7580  addcnsr  7606  mulcnsr  7607  mulcnsrec  7615  axmulcom  7643  rereceu  7661  axarch  7663  axcaucvglemres  7671  axpre-suploclemres  7673  lelttr  7816  ltletr  7817  addcan  7906  addcan2  7907  addsub4  7969  ltadd2  8145  le2add  8170  lt2add  8171  lt2sub  8186  le2sub  8187  eqord1  8209  rereim  8311  apreap  8312  apreim  8328  mulreim  8329  apcotr  8332  apadd1  8333  addext  8335  apneg  8336  mulext1  8337  mulext  8339  ltleap  8356  aprcl  8370  mulap0  8375  mulcanapd  8382  rec11ap  8430  rec11rap  8431  divdivdivap  8433  ddcanap  8446  divadddivap  8447  prodgt0gt0  8566  prodgt0  8567  prodge0  8569  lemulge11  8581  lt2mul2div  8594  ltrec  8598  lerec  8599  lerec2  8604  ledivp1  8618  mulle0r  8659  nn0ge0div  9089  suprzclex  9100  qapne  9380  xrlelttr  9529  xrltletr  9530  xrre3  9545  xrrege0  9548  xaddge0  9601  xle2add  9602  xlt2add  9603  fzass4  9782  fzrev  9804  elfz1b  9810  eluzgtdifelfzo  9914  fzocatel  9916  exbtwnzlemex  9967  rebtwn2z  9972  modqid  10062  modqcyc  10072  modqaddabs  10075  modqaddmod  10076  mulqaddmodid  10077  modqadd2mod  10087  modqltm1p1mod  10089  modqsubmod  10095  modqsubmodmod  10096  modaddmodup  10100  modqmulmod  10102  modqmulmodr  10103  modqaddmulmod  10104  modqsubdir  10106  frec2uzisod  10120  uzennn  10149  iseqovex  10169  seqvalcd  10172  seqf  10174  seqovcd  10176  seq3shft2  10186  monoord  10189  iseqf1olemnab  10201  seq3distr  10226  expnegzap  10267  ltexp2a  10285  le2sq2  10308  bernneq  10352  expnlbnd2  10357  nn0opth2  10410  faclbnd  10427  bcval5  10449  hashcl  10467  hashen  10470  fihashdom  10489  hashunlem  10490  hashun  10491  hashxp  10512  fimaxq  10513  zfz1isolem1  10523  zfz1iso  10524  seq3coll  10525  cvg1nlemres  10697  cvg1n  10698  resqrexlemp1rp  10718  resqrexlemoverl  10733  resqrexlemex  10737  sqrtsq  10756  abslt  10800  absle  10801  abs3lem  10823  maxleastlt  10927  maxltsup  10930  fimaxre2  10938  negfi  10939  xrmaxleastlt  10965  xrmaxltsup  10967  xrmaxaddlem  10969  2clim  11010  climcn2  11018  addcn2  11019  mulcn2  11021  reccn2ap  11022  climge0  11034  climcau  11056  summodclem2  11091  summodc  11092  zsumdc  11093  fsumf1o  11099  fisumss  11101  fsum3cvg3  11105  fsumcl2lem  11107  fsumadd  11115  mptfzshft  11151  fsumrev  11152  fsummulc2  11157  fsumconst  11163  modfsummod  11167  fsumrelem  11180  binom  11193  cvgratnn  11240  mertenslemub  11243  efcllem  11264  tanaddaplem  11344  moddvds  11398  dvdsflip  11445  oexpneg  11470  nn0o  11500  fldivndvdslt  11528  zsupcllemstep  11534  zsupcllemex  11535  zssinfcl  11537  bezoutlemnewy  11580  bezoutlemstep  11581  bezoutlemeu  11591  dfgcd3  11594  dfgcd2  11598  dvdsmulgcd  11609  bezoutr  11616  lcmgcdlem  11654  coprmdvds2  11670  qredeu  11674  rpdvds  11676  cncongr1  11680  prmind2  11697  isprm6  11721  oddpwdclemdc  11746  nonsq  11780  hashdvds  11792  crth  11795  hashgcdlem  11798  hashgcdeq  11799  ennnfonelemg  11811  ennnfonelemex  11822  ennnfonelemrnh  11824  ennnfonelemf1  11826  ennnfonelemrn  11827  ennnfonelemdm  11828  ennnfonelemim  11832  ennnfone  11833  ctinf  11838  ctiunctlemfo  11847  isstruct2r  11865  setscom  11894  iuncld  12179  ssnei2  12221  topssnei  12226  restopnb  12245  cnfval  12258  cnpfval  12259  iscnp4  12282  cnptopco  12286  cncnpi  12292  cncnp  12294  cnconst2  12297  cnrest2  12300  cnptoprest  12303  cnptoprest2  12304  cnpdis  12306  lmss  12310  lmtopcnp  12314  neitx  12332  txcnp  12335  txrest  12340  txdis1cn  12342  txlm  12343  cnmpt21  12355  imasnopn  12363  xmetres2  12443  blvalps  12452  blval  12453  elbl2ps  12456  elbl2  12457  blhalf  12472  blssexps  12493  blssex  12494  ssblex  12495  blin2  12496  bdmetval  12564  xmetxp  12571  xmettx  12574  metcnpi3  12581  txmetcnp  12582  addcncntoplem  12615  fsumcncntop  12620  elcncf2  12625  mulc1cncf  12640  cncfco  12642  cncfmet  12643  cncfmptc  12646  mulcncf  12655  dedekindeulemub  12660  dedekindeulemloc  12661  dedekindeulemlu  12663  dedekindeu  12665  dedekindicclemub  12669  dedekindicclemloc  12670  dedekindicclemlu  12672  dedekindicc  12674  limcimo  12686  cnplimccntop  12691  limccnp2lem  12697  limccnp2cntop  12698  dvfvalap  12702  dveflem  12738  nnti  13002  pwtrufal  13003  pwf1oexmid  13005  qdencn  13033  cvgcmp2n  13039  trilpolemlt1  13045  supfz  13048  inffz  13049
  Copyright terms: Public domain W3C validator