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

Theorem simprr 531
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 491 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem is referenced by:  simp1rr  1063  simp2rr  1067  simp3rr  1071  disjiun  3995  reg2exmidlema  4530  reg3exmidlemwe  4575  nnsucpred  4613  iotam  5204  fvmptt  5603  fcof1  5778  fliftfun  5791  isotr  5811  riotass2  5851  acexmidlemab  5863  ovmpodf  6000  fnmpoovd  6210  1stconst  6216  2ndconst  6217  cnvf1olem  6219  f1od2  6230  smoiso  6297  tfrcldm  6358  tfrcl  6359  nntr2  6498  swoer  6557  erinxp  6603  ecopovsymg  6628  th3qlem1  6631  f1imaen2g  6787  mapdom1g  6841  fict  6862  fidifsnen  6864  dif1enen  6874  fiunsnnn  6875  fisbth  6877  findcard2d  6885  findcard2sd  6886  diffifi  6888  ac6sfi  6892  fimax2gtri  6895  nnwetri  6909  unsnfi  6912  unsnfidcex  6913  unsnfidcel  6914  fisseneq  6925  ssfirab  6927  fidcenumlemrk  6947  fidcenumlemr  6948  sbthlemi6  6955  sbthlemi8  6957  isbth  6960  fiuni  6971  supmaxti  6997  infminti  7020  ordiso2  7028  eldju2ndl  7065  eldju2ndr  7066  omp1eomlem  7087  difinfsnlem  7092  difinfinf  7094  ctmlemr  7101  ctssdccl  7104  fodjum  7138  fodju0  7139  omniwomnimkv  7159  exmidfodomrlemrALT  7196  acfun  7200  exmidaclem  7201  netap  7244  exmidmotap  7251  ccfunen  7254  cc1  7255  cc2lem  7256  dfplpq2  7344  dfmpq2  7345  mulpipqqs  7363  distrnqg  7377  enq0sym  7422  enq0tr  7424  distrnq0  7449  prarloclem3  7487  genplt2i  7500  addlocpr  7526  prmuloc  7556  distrlem1prl  7572  distrlem1pru  7573  ltexprlemopl  7591  ltexprlemopu  7593  ltexprlemfl  7599  ltexprlemrl  7600  ltexprlemfu  7601  ltexprlemru  7602  addcanprleml  7604  addcanprlemu  7605  ltaprg  7609  prplnqu  7610  addextpr  7611  recexprlemdisj  7620  recexprlemloc  7621  aptiprleml  7629  aptiprlemu  7630  ltmprr  7632  archpr  7633  cauappcvgprlemopl  7636  cauappcvgprlemopu  7638  cauappcvgprlemdisj  7641  cauappcvgprlemloc  7642  cauappcvgprlem1  7649  cauappcvgprlemlim  7651  caucvgprlemnkj  7656  caucvgprlemopl  7659  caucvgprlemopu  7661  caucvgprlemdisj  7664  caucvgprlemloc  7665  caucvgprprlemnkltj  7679  caucvgprprlemnkeqj  7680  caucvgprprlemnjltk  7681  caucvgprprlemml  7684  caucvgprprlemmu  7685  caucvgprprlemopl  7687  caucvgprprlemopu  7689  caucvgprprlemdisj  7692  caucvgprprlemloc  7693  caucvgprprlemaddq  7698  suplocexprlemrl  7707  suplocexprlemmu  7708  suplocexprlemru  7709  suplocexprlemdisj  7710  suplocexprlemloc  7711  suplocexprlemex  7712  suplocexprlemub  7713  recexgt0sr  7763  mulgt0sr  7768  prsrriota  7778  suplocsrlem  7798  addcnsr  7824  mulcnsr  7825  mulcnsrec  7833  axmulcom  7861  rereceu  7879  axarch  7881  axcaucvglemres  7889  axpre-suploclemres  7891  lelttr  8036  ltletr  8037  addcan  8127  addcan2  8128  addsub4  8190  ltadd2  8366  le2add  8391  lt2add  8392  lt2sub  8407  le2sub  8408  eqord1  8430  rereim  8533  apreap  8534  apreim  8550  mulreim  8551  apcotr  8554  apadd1  8555  addext  8557  apneg  8558  mulext1  8559  mulext  8561  ltleap  8579  aprcl  8593  mulap0  8600  mulcanapd  8607  recapb  8617  rec11ap  8656  rec11rap  8657  divdivdivap  8659  ddcanap  8672  divadddivap  8673  prodgt0gt0  8797  prodgt0  8798  prodge0  8800  lemulge11  8812  lt2mul2div  8825  ltrec  8829  lerec  8830  lerec2  8835  ledivp1  8849  mulle0r  8890  nn0ge0div  9329  suprzclex  9340  qapne  9628  xrlelttr  9793  xrltletr  9794  xrre3  9809  xrrege0  9812  xaddge0  9865  xle2add  9866  xlt2add  9867  fzass4  10048  fzrev  10070  elfz1b  10076  eluzgtdifelfzo  10183  fzocatel  10185  exbtwnzlemex  10236  rebtwn2z  10241  modqid  10335  modqcyc  10345  modqaddabs  10348  modqaddmod  10349  mulqaddmodid  10350  modqadd2mod  10360  modqltm1p1mod  10362  modqsubmod  10368  modqsubmodmod  10369  modaddmodup  10373  modqmulmod  10375  modqmulmodr  10376  modqaddmulmod  10377  modqsubdir  10379  frec2uzisod  10393  uzennn  10422  iseqovex  10442  seqvalcd  10445  seqf  10447  seqovcd  10449  seq3shft2  10459  monoord  10462  iseqf1olemnab  10474  seq3distr  10499  expnegzap  10540  ltexp2a  10558  le2sq2  10581  bernneq  10626  expnlbnd2  10631  nn0ltexp2  10674  nn0opth2  10688  faclbnd  10705  bcval5  10727  hashcl  10745  hashen  10748  fihashdom  10767  hashunlem  10768  hashun  10769  hashxp  10790  fimaxq  10791  zfz1isolem1  10804  zfz1iso  10805  seq3coll  10806  cvg1nlemres  10978  cvg1n  10979  resqrexlemp1rp  10999  resqrexlemoverl  11014  resqrexlemex  11018  sqrtsq  11037  abslt  11081  absle  11082  abs3lem  11104  maxleastlt  11208  maxltsup  11211  fimaxre2  11219  negfi  11220  xrmaxleastlt  11248  xrmaxltsup  11250  xrmaxaddlem  11252  2clim  11293  climcn2  11301  addcn2  11302  mulcn2  11304  reccn2ap  11305  climge0  11317  climcau  11339  summodclem2  11374  summodc  11375  zsumdc  11376  fsumf1o  11382  fisumss  11384  fsum3cvg3  11388  fsumcl2lem  11390  fsumadd  11398  mptfzshft  11434  fsumrev  11435  fsummulc2  11440  fsumconst  11446  modfsummod  11450  fsumrelem  11463  binom  11476  cvgratnn  11523  mertenslemub  11526  prodmodclem2  11569  prodmodc  11570  zproddc  11571  fprodf1o  11580  fprodssdc  11582  fprodmul  11583  fprodcl2lem  11597  fprodrev  11611  fprodconst  11612  fprodap0  11613  fprodrec  11621  fprodap0f  11628  fprodle  11632  fprodmodd  11633  efcllem  11651  tanaddaplem  11730  moddvds  11790  dvdsflip  11840  oexpneg  11865  nn0o  11895  fldivndvdslt  11923  zsupcllemstep  11929  zsupcllemex  11930  zssinfcl  11932  suprzubdc  11936  bezoutlemnewy  11980  bezoutlemstep  11981  bezoutlemeu  11991  dfgcd3  11994  dfgcd2  11998  dvdsmulgcd  12009  bezoutr  12016  lcmgcdlem  12060  coprmdvds2  12076  qredeu  12080  rpdvds  12082  cncongr1  12086  prmind2  12103  isprm5lem  12124  isprm6  12130  oddpwdclemdc  12156  nonsq  12190  hashdvds  12204  crth  12207  eulerthlemh  12214  prmdiveq  12219  hashgcdlem  12221  hashgcdeq  12222  nnnn0modprm0  12238  pclemub  12270  pceu  12278  pcmul  12284  pcqmul  12286  pcgcd1  12310  pc2dvds  12312  difsqpwdvds  12320  pcmpt  12324  prmpwdvds  12336  1arith  12348  mul4sq  12375  ennnfonelemg  12387  ennnfonelemex  12398  ennnfonelemrnh  12400  ennnfonelemf1  12402  ennnfonelemrn  12403  ennnfonelemdm  12404  ennnfonelemim  12408  ennnfone  12409  ctinf  12414  ctiunctlemfo  12423  nninfdclemcl  12432  nninfdclemf  12433  nninfdclemp1  12434  unbendc  12438  isstruct2r  12456  setscom  12485  opifismgmdc  12682  grprinvlem  12696  mndpropd  12733  issubmnd  12735  mhmf1o  12751  0mhm  12763  mhmco  12764  mhmima  12765  mhmeql  12766  grprcan  12800  grpinvid1  12814  grpinvid2  12815  grplcan  12821  grplmulf1o  12833  grpnpncan0  12855  dfgrp3mlem  12857  grplactcnv  12861  mulgval  12875  mulgfng  12876  mulg1  12879  mulgnnp1  12880  mulgneg  12890  mulgnndir  12900  mulgdirlem  12902  mulgnn0ass  12907  mulgass  12908  ablpncan3  12947  srglmhm  13002  srgrmhm  13003  ringpropd  13043  dvdsrvald  13087  dvdsrd  13088  dvdsrex  13092  dvdsrtr  13095  unitpropdg  13140  iuncld  13282  ssnei2  13324  topssnei  13329  restopnb  13348  cnfval  13361  cnpfval  13362  iscnp4  13385  cnptopco  13389  cncnpi  13395  cncnp  13397  cnconst2  13400  cnrest2  13403  cnptoprest  13406  cnptoprest2  13407  cnpdis  13409  lmss  13413  lmtopcnp  13417  neitx  13435  txcnp  13438  txrest  13443  txdis1cn  13445  txlm  13446  cnmpt21  13458  imasnopn  13466  xmetres2  13546  blvalps  13555  blval  13556  elbl2ps  13559  elbl2  13560  blhalf  13575  blssexps  13596  blssex  13597  ssblex  13598  blin2  13599  bdmetval  13667  xmetxp  13674  xmettx  13677  metcnpi3  13684  txmetcnp  13685  addcncntoplem  13718  fsumcncntop  13723  elcncf2  13728  mulc1cncf  13743  cncfco  13745  cncfmet  13746  cncfmptc  13749  mulcncf  13758  dedekindeulemub  13763  dedekindeulemloc  13764  dedekindeulemlu  13766  dedekindeu  13768  dedekindicclemub  13772  dedekindicclemloc  13773  dedekindicclemlu  13775  dedekindicclemicc  13777  dedekindicc  13778  ivthinclemlopn  13781  ivthinclemuopn  13783  limcimo  13801  cnplimccntop  13806  limccnp2lem  13812  limccnp2cntop  13813  dvfvalap  13817  dveflem  13854  reeff1olem  13859  reeff1oleme  13860  eflt  13863  sin0pilem2  13870  pilem3  13871  ioocosf1o  13942  cxplt  14003  cxple  14004  cxplt3  14007  apcxp2  14025  rprelogbmul  14040  rprelogbdiv  14042  logbgt0b  14051  logbgcd1irrap  14055  lgsdir2lem5  14100  lgsdi  14105  lgsne0  14106  2sqlem6  14123  2sqlem8  14126  2sqlem9  14127  2sqlem10  14128  nnti  14400  pwtrufal  14403  pwf1oexmid  14405  sssneq  14407  qdencn  14431  cvgcmp2n  14437  trilpolemlt1  14445  trirec0  14448  redc0  14461  reap0  14462  nconstwlpolemgt0  14467  supfz  14472  inffz  14473
  Copyright terms: Public domain W3C validator