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

Theorem simplr 497
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 473 1 (((𝜑𝜓) ∧ 𝜒) → 𝜓)
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:  simp1lr  1005  simp2lr  1009  simp3lr  1013  bilukdc  1330  intab  3700  exmid01  4005  exmidundif  4008  frirrg  4150  reg2exmidlema  4322  imadiflem  5055  fvco4  5333  fvmptt  5351  fcoconst  5425  f1imass  5508  fcof1  5517  fliftfun  5530  riotass2  5589  ovmpt2dxf  5721  dftpos4  5976  tfrlem1  6021  tfrlem3ag  6022  tfrlemibacc  6039  tfrlemibfn  6041  tfrlemi1  6045  tfrlemi14d  6046  tfr1onlem3ag  6050  tfr1onlembacc  6055  tfr1onlembfn  6057  tfr1onlemaccex  6061  tfrcllembacc  6068  tfrcllembfn  6070  tfrcllemaccex  6074  frecabcl  6112  dcdifsnid  6211  nnm00  6234  ecopovsymg  6337  ecopoverg  6339  th3qlem1  6340  mapss  6394  f1imaen2g  6456  xpen  6507  xpmapenlem  6511  phpm  6527  fidifsnen  6532  dif1enen  6542  fiunsnnn  6543  fin0  6547  fin0or  6548  findcard2d  6553  findcard2sd  6554  diffifi  6556  isinfinf  6559  tridc  6561  fimax2gtrilemstep  6562  fimax2gtri  6563  en2eqpr  6569  onunsnss  6573  unsnfidcex  6576  unsnfidcel  6577  undifdcss  6579  unfiin  6582  fisseneq  6586  ssfirab  6587  f1finf1o  6599  suplub2ti  6633  supisolem  6640  ordiso2  6665  djudom  6724  enomnilem  6731  finomni  6733  exmidomni  6735  fodjuomnilem0  6739  exmidfodomrlemr  6765  exmidfodomrlemrALT  6766  dfplpq2  6850  dfmpq2  6851  mulpipqqs  6869  nqpi  6874  distrnqg  6883  prarloclemarch  6914  enq0tr  6930  nqnq0pi  6934  nq0nn  6938  nnnq0lem1  6942  prarloclemup  6991  prarloclem3  6993  prarloclemcalc  6998  genplt2i  7006  addnqprllem  7023  addnqprulem  7024  appdivnq  7059  distrlem1prl  7078  distrlem1pru  7079  ltaddpr  7093  ltexprlemlol  7098  ltexprlemupu  7100  ltexprlemdisj  7102  addcanprleml  7110  ltaprlem  7114  addextpr  7117  recexprlemopu  7123  recexprlemdisj  7126  recexprlem1ssl  7129  aptiprleml  7135  cauappcvgprlemm  7141  cauappcvgprlemopl  7142  cauappcvgprlemlol  7143  cauappcvgprlemopu  7144  cauappcvgprlemdisj  7147  cauappcvgprlemladdfu  7150  cauappcvgprlemladdfl  7151  cauappcvgprlemladdru  7152  cauappcvgprlemladdrl  7153  caucvgprlemm  7164  caucvgprlemopl  7165  caucvgprlemlol  7166  caucvgprlemopu  7167  caucvgprlemladdfu  7173  caucvgprprlemml  7190  caucvgprprlemopl  7193  caucvgprprlemlol  7194  caucvgprprlemopu  7195  caucvgprprlemexbt  7202  prsrlem1  7225  recexgt0sr  7256  mulgt0sr  7260  archsr  7264  caucvgsrlemcau  7275  caucvgsrlemoffcau  7280  caucvgsrlemoffres  7282  addcnsr  7308  mulcnsr  7309  mulcnsrec  7317  axmulcom  7343  nntopi  7366  axcaucvglemcau  7370  axcaucvglemres  7371  cnegexlem2  7595  cnegexlem3  7596  addsub4  7662  le2add  7859  lt2add  7860  lt2sub  7875  le2sub  7876  rereim  7997  apreim  8014  mulreim  8015  apcotr  8018  apadd1  8019  addext  8021  mulext1  8023  mulext  8025  apti  8033  receuap  8070  rec11rap  8110  divdivdivap  8112  divadddivap  8126  divsubdivap  8127  rerecclap  8129  recgt0  8239  prodgt0gt0  8240  prodgt0  8241  prodge0  8243  lemulge11  8255  lt2mul2div  8268  ltrec  8272  lerec  8273  ltrec1  8277  lediv2a  8284  mulle0r  8333  zdiv  8760  eluzuzle  8952  supinfneg  9008  infsupneg  9009  xrltso  9191  z2ge  9213  ixxss1  9247  ixxss2  9248  elico2  9280  iccsupr  9309  fzass4  9400  fzrev  9421  fz0fzelfz0  9459  fzocatel  9531  elfzomelpfzo  9563  exbtwnzlemstep  9580  rebtwn2zlemstep  9585  qbtwnxr  9590  apbtwnz  9602  btwnzge0  9628  modqid  9677  modqcyc  9687  modqcyc2  9688  modqaddabs  9690  modqaddmod  9691  mulqaddmodid  9692  modqmuladd  9694  modqltm1p1mod  9704  modqsubmod  9710  modqsubmodmod  9711  modaddmodlo  9716  modqmulmod  9717  modqmulmodr  9718  modqsubdir  9721  addmodlteq  9726  iseqf1olemab  9815  iseqf1olemmo  9818  iseqf1olemjpcl  9821  iseqf1olemqpcl  9822  expival  9848  expcl2lemap  9858  expap0  9876  expnegzap  9880  expmul  9891  leexp1a  9901  expnbnd  9966  nn0opth2  10021  facndiv  10036  faclbnd  10038  ibcval5  10060  bcpasc  10063  hashennnuni  10076  hashunlem  10101  hashunsng  10104  hashprg  10105  fiprsshashgt1  10114  hashxp  10123  fimaxq  10124  zfz1isolemiso  10133  zfz1isolem1  10134  iseqcoll  10136  shftlem  10139  shftfvalg  10141  shftfval  10144  2shfti  10154  caucvgrelemrec  10300  caucvgrelemcau  10301  caucvgre  10302  cvg1nlemcau  10305  cvg1nlemres  10306  resqrexlemcalc3  10337  resqrexlemcvg  10340  resqrexlemglsq  10343  resqrexlemga  10344  sqrtsq  10365  leabs  10395  absexpzap  10401  abslt  10409  absle  10410  abssubap0  10411  caubnd2  10438  icodiamlt  10501  maxleim  10526  maxabslemval  10529  maxleastlt  10536  rexico  10542  fimaxre2  10544  minmax  10547  climuni  10567  climshftlemg  10576  iiserex  10612  climcau  10619  climrecvg1n  10620  climcvg1nlem  10621  sumeq2  10631  isummolem3  10652  zisum  10656  isumss  10662  zdvdsdc  10684  dvds2ln  10696  dvdsle  10712  dvdsext  10723  divalglemeunn  10788  divalglemex  10789  divalglemeuneg  10790  zsupcllemstep  10808  dvdsbnd  10815  gcdsupex  10816  gcdsupcl  10817  dvdslegcd  10823  bezoutlemnewy  10852  bezoutlemstep  10853  bezoutlemmain  10854  bezoutlemzz  10858  bezoutlembz  10860  bezoutlembi  10861  bezoutlemle  10864  dfgcd3  10866  bezout  10867  dfgcd2  10870  dvdsmulgcd  10881  bezoutr  10888  lcmval  10912  lcmcllem  10916  lcmneg  10923  ncoprmgcdne1b  10938  isprm2lem  10965  prmind2  10969  dvdsnprmd  10974  prmdvdsexp  10994  sqrt2irr  11008  oddpwdclemxy  11014  oddpwdclemdc  11018  nonsq  11052  peano4nninf  11326  nninfalllemn  11328  nninfalllem1  11329  nninfall  11330  nninfsellemeq  11336  nninfsellemqall  11337
  Copyright terms: Public domain W3C validator