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

Theorem simplr 504
Description: Simplification of a conjunction. (Contributed by NM, 20-Mar-2007.)
Assertion
Ref Expression
simplr (((𝜑𝜓) ∧ 𝜒) → 𝜓)

Proof of Theorem simplr
StepHypRef Expression
1 id 19 . 2 (𝜓𝜓)
21ad2antlr 480 1 (((𝜑𝜓) ∧ 𝜒) → 𝜓)
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:  simp1lr  1030  simp2lr  1034  simp3lr  1038  bilukdc  1359  dcun  3443  intab  3770  exmid01  4091  exmidundif  4099  exmidundifim  4100  frirrg  4242  reg2exmidlema  4419  imadiflem  5172  fvco4  5461  fvmptt  5480  fcoconst  5559  f1imass  5643  fcof1  5652  fliftfun  5665  riotass2  5724  ovmpodxf  5864  dftpos4  6128  tfrlem1  6173  tfrlem3ag  6174  tfrlemibacc  6191  tfrlemibfn  6193  tfrlemi1  6197  tfrlemi14d  6198  tfr1onlem3ag  6202  tfr1onlembacc  6207  tfr1onlembfn  6209  tfr1onlemaccex  6213  tfrcllembacc  6220  tfrcllembfn  6222  tfrcllemaccex  6226  frecabcl  6264  nntr2  6367  dcdifsnid  6368  nnm00  6393  ecopovsymg  6496  ecopoverg  6498  th3qlem1  6499  mapss  6553  f1imaen2g  6655  xpen  6707  xpmapenlem  6711  phpm  6727  fidifsnen  6732  dif1enen  6742  fiunsnnn  6743  fin0  6747  fin0or  6748  findcard2d  6753  findcard2sd  6754  diffifi  6756  isinfinf  6759  tridc  6761  fimax2gtrilemstep  6762  fimax2gtri  6763  en2eqpr  6769  onunsnss  6773  unsnfidcex  6776  unsnfidcel  6777  undifdcss  6779  unfiin  6782  fisseneq  6788  ssfirab  6790  f1finf1o  6803  fidcenumlemrks  6809  fidcenumlemrk  6810  fidcenumlemr  6811  fidcenum  6812  suplub2ti  6856  supisolem  6863  ordiso2  6888  djudom  6946  omp1eomlem  6947  difinfsnlem  6952  difinfinf  6954  ctm  6962  ctssdclemn0  6963  enumct  6968  enomnilem  6978  finomni  6980  exmidomni  6982  fodju0  6987  ismkvnex  6997  exmidfodomrlemr  7026  exmidfodomrlemrALT  7027  exmidaclem  7032  dfplpq2  7130  dfmpq2  7131  mulpipqqs  7149  nqpi  7154  distrnqg  7163  prarloclemarch  7194  enq0tr  7210  nqnq0pi  7214  nq0nn  7218  nnnq0lem1  7222  prarloclemup  7271  prarloclem3  7273  prarloclemcalc  7278  genplt2i  7286  addnqprllem  7303  addnqprulem  7304  appdivnq  7339  distrlem1prl  7358  distrlem1pru  7359  ltaddpr  7373  ltexprlemlol  7378  ltexprlemupu  7380  ltexprlemdisj  7382  addcanprleml  7390  ltaprlem  7394  addextpr  7397  recexprlemopu  7403  recexprlemdisj  7406  recexprlem1ssl  7409  aptiprleml  7415  cauappcvgprlemm  7421  cauappcvgprlemopl  7422  cauappcvgprlemlol  7423  cauappcvgprlemopu  7424  cauappcvgprlemdisj  7427  cauappcvgprlemladdfu  7430  cauappcvgprlemladdfl  7431  cauappcvgprlemladdru  7432  cauappcvgprlemladdrl  7433  caucvgprlemm  7444  caucvgprlemopl  7445  caucvgprlemlol  7446  caucvgprlemopu  7447  caucvgprlemladdfu  7453  caucvgprprlemml  7470  caucvgprprlemopl  7473  caucvgprprlemlol  7474  caucvgprprlemopu  7475  caucvgprprlemexbt  7482  suplocexprlemru  7495  suplocexprlemloc  7497  suplocexprlemub  7499  suplocexprlemlub  7500  prsrlem1  7518  recexgt0sr  7549  mulgt0sr  7554  archsr  7558  caucvgsrlemcau  7569  caucvgsrlemoffcau  7574  caucvgsrlemoffres  7576  suplocsrlemb  7582  suplocsrlempr  7583  suplocsrlem  7584  addcnsr  7610  mulcnsr  7611  mulcnsrec  7619  axmulcom  7647  nntopi  7670  axcaucvglemcau  7674  axcaucvglemres  7675  axpre-suploclemres  7677  axpre-suploc  7678  axsuploc  7805  ltntri  7858  cnegexlem2  7906  cnegexlem3  7907  addsub4  7973  le2add  8174  lt2add  8175  lt2sub  8190  le2sub  8191  rereim  8315  apreim  8332  mulreim  8333  apcotr  8336  apadd1  8337  addext  8339  mulext1  8341  mulext  8343  apti  8351  receuap  8397  rec11rap  8438  divdivdivap  8440  divadddivap  8454  divsubdivap  8455  rerecclap  8457  recgt0  8572  prodgt0gt0  8573  prodgt0  8574  prodge0  8576  lemulge11  8588  lt2mul2div  8601  ltrec  8605  lerec  8606  ltrec1  8610  lediv2a  8617  mulle0r  8666  sup3exmid  8679  zdiv  9097  eluzuzle  9290  supinfneg  9346  infsupneg  9347  xrltso  9537  npnflt  9553  nmnfgt  9556  z2ge  9564  xaddf  9582  xaddval  9583  xpncan  9609  xleadd1a  9611  xltadd1  9614  xaddge0  9616  xle2add  9617  xleaddadd  9625  ixxss1  9642  ixxss2  9643  elico2  9675  iccsupr  9704  fzass4  9797  fzrev  9819  fz0fzelfz0  9859  fzocatel  9931  elfzomelpfzo  9963  exbtwnzlemstep  9980  rebtwn2zlemstep  9985  qbtwnxr  9990  apbtwnz  10002  btwnzge0  10028  modqid  10077  modqcyc  10087  modqcyc2  10088  modqaddabs  10090  modqaddmod  10091  mulqaddmodid  10092  modqmuladd  10094  modqltm1p1mod  10104  modqsubmod  10110  modqsubmodmod  10111  modaddmodlo  10116  modqmulmod  10117  modqmulmodr  10118  modqsubdir  10121  addmodlteq  10126  iseqf1olemab  10217  iseqf1olemmo  10220  iseqf1olemjpcl  10223  iseqf1olemqpcl  10224  exp3val  10250  expcl2lemap  10260  expap0  10278  expnegzap  10282  expmul  10293  leexp1a  10303  expnbnd  10370  nn0opth2  10425  facndiv  10440  faclbnd  10442  bcval5  10464  bcpasc  10467  hashennnuni  10480  hashunlem  10505  hashunsng  10508  hashprg  10509  fiprsshashgt1  10518  hashxp  10527  fimaxq  10528  zfz1isolemiso  10537  zfz1isolem1  10538  seq3coll  10540  shftlem  10543  shftfvalg  10545  shftfval  10548  2shfti  10558  caucvgrelemrec  10706  caucvgrelemcau  10707  caucvgre  10708  cvg1nlemcau  10711  cvg1nlemres  10712  resqrexlemcalc3  10743  resqrexlemcvg  10746  resqrexlemglsq  10749  resqrexlemga  10750  sqrtsq  10771  leabs  10801  absexpzap  10807  abslt  10815  absle  10816  abssubap0  10817  caubnd2  10844  icodiamlt  10907  maxleim  10932  maxabslemval  10935  maxleastlt  10942  rexico  10948  zmaxcl  10951  fimaxre2  10953  minmax  10956  xrmaxleim  10968  xrmaxiflemcl  10969  xrmaxifle  10970  xrmaxiflemlub  10972  xrmaxiflemval  10974  xrmaxleastlt  10980  xrmaxltsup  10982  xrmaxadd  10985  xrminmax  10989  xrbdtri  11000  climuni  11017  climshftlemg  11026  iserex  11063  climcau  11071  climrecvg1n  11072  climcvg1nlem  11073  sumeq2  11083  summodclem3  11104  zsumdc  11108  isumss  11115  fisumss  11116  sumsnf  11133  fsumconst  11178  modfsummod  11182  fsum00  11186  fsumabs  11189  fsumrelem  11195  fsumiun  11201  isumsplit  11215  divcnv  11221  geo2sum  11238  geoisumr  11242  cvgratz  11256  tanaddap  11360  zdvdsdc  11426  dvds2ln  11438  dvdsle  11454  dvdsext  11465  divalglemeunn  11530  divalglemex  11531  divalglemeuneg  11532  zsupcllemstep  11550  dvdsbnd  11557  gcdsupex  11558  gcdsupcl  11559  dvdslegcd  11565  bezoutlemnewy  11596  bezoutlemstep  11597  bezoutlemmain  11598  bezoutlemzz  11602  bezoutlembz  11604  bezoutlembi  11605  bezoutlemle  11608  dfgcd3  11610  bezout  11611  dfgcd2  11614  dvdsmulgcd  11625  bezoutr  11632  lcmval  11656  lcmcllem  11660  lcmneg  11667  ncoprmgcdne1b  11682  isprm2lem  11709  prmind2  11713  dvdsnprmd  11718  prmdvdsexp  11738  sqrt2irr  11752  oddpwdclemxy  11758  oddpwdclemdc  11762  nonsq  11796  ennnfonelemkh  11836  ennnfonelemhf1o  11837  ennnfonelemhom  11839  ennnfonelemfun  11841  ennnfonelemf1  11842  ennnfonelemim  11848  exmidunben  11850  ctiunctlemfo  11863  isstruct2r  11881  opnssneib  12236  restbasg  12248  restopn2  12263  iscnp4  12298  cnss2  12307  cnconst2  12313  cnptopresti  12318  cnptoprest2  12320  neitx  12348  uptx  12354  txrest  12356  txdis1cn  12358  xmetres2  12459  xblss2ps  12484  blhalf  12488  blssps  12507  blss  12508  blssexps  12509  blssex  12510  blin2  12512  metequiv2  12576  bdmetval  12580  metcnp3  12591  metcnp  12592  metcn  12594  metcnpi  12595  metcnpi2  12596  txmetcnp  12598  txmetcn  12599  qtopbas  12602  tgqioo  12627  fsumcncntop  12636  elcncf2  12641  mulcncflem  12670  mulcncf  12671  suplociccreex  12682  limcdifap  12711  cnplimcim  12716  cnplimccntop  12719  limccnpcntop  12724  dvcj  12753  dveflem  12766  sin0pilem1  12773  ptolemy  12816  coseq0q4123  12826  coseq0negpitopi  12828  pwle2  13089  pwf1oexmid  13090  subctctexmid  13092  peano4nninf  13096  nninfalllemn  13098  nninfalllem1  13099  nninfall  13100  nninfsellemeq  13106  nninfsellemqall  13107  sbthom  13117  refeq  13119  isomninnlem  13121  trilpolemeq1  13129  trilpolemlt1  13130
  Copyright terms: Public domain W3C validator