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

Theorem simprd 113
Description: Deduction eliminating a conjunct. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
Hypothesis
Ref Expression
simprd.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
simprd (𝜑𝜒)

Proof of Theorem simprd
StepHypRef Expression
1 simprd.1 . 2 (𝜑 → (𝜓𝜒))
2 simpr 109 . 2 ((𝜓𝜒) → 𝜒)
31, 2syl 14 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-ia2 106
This theorem is referenced by:  bi2  129  simprbi  273  simplbda  381  simp2  982  simp3  983  sbh  1749  eldifbd  3083  unssbd  3254  opth  4162  potr  4233  frind  4277  brrelex2  4583  funinsn  5175  feu  5308  fcnvres  5309  fun11iun  5391  elmpocl2  5973  oprssdmm  6072  tfrlem1  6208  tfrlemisucfn  6224  tfrlemisucaccv  6225  tfrlemibxssdm  6227  tfrlemibfn  6228  tfrlemi14d  6233  swoer  6460  elmapssres  6570  mapsspm  6579  pmsspw  6580  mapss  6588  dom0  6735  xpf1o  6741  sbthlemi8  6855  sbthlemi9  6856  supelti  6892  supisoti  6900  djulclb  6943  cardcl  7049  isnumi  7050  cardval3ex  7053  exmidonfinlem  7061  en2eleq  7063  acfun  7075  exmidaclem  7076  ccfunen  7091  indpi  7169  dfplpq2  7181  ltbtwnnq  7243  enq0tr  7261  nqnq0pi  7265  elnp1st2nd  7303  prcunqu  7312  prnmaxl  7315  prloc  7318  genpcuu  7347  addnqprllem  7354  addlocprlemeq  7360  addlocprlemgt  7361  addlocpr  7363  nqprxx  7373  gtnqex  7377  appdivnq  7390  prmuloclemcalc  7392  prmuloc  7393  mullocprlem  7397  ltprordil  7416  ltnqpri  7421  ltexprlemm  7427  ltexprlemopl  7428  ltexprlemlol  7429  ltexprlemopu  7430  ltexprlemupu  7431  ltexprlemdisj  7433  ltexprlemloc  7434  ltexprlemfl  7436  ltexprlemrl  7437  ltexprlemfu  7438  ltexprlemru  7439  ltexpri  7440  recexprlemell  7449  recexprlemelu  7450  recexprlemloc  7458  recexprlempr  7459  recexprlem1ssl  7460  recexprlem1ssu  7461  recexprlemss1l  7462  aptipr  7468  cauappcvgprlemlol  7474  cauappcvgprlemupu  7476  cauappcvgprlemladdfu  7481  cauappcvgprlemladdfl  7482  cauappcvgprlemladdrl  7484  caucvgprlemnkj  7493  caucvgprlemnbj  7494  caucvgprlemlol  7497  caucvgprlemupu  7499  caucvgprlemladdfu  7504  caucvgprlem1  7506  caucvgprlem2  7507  caucvgprprlemnjltk  7518  caucvgprprlemnbj  7520  caucvgprprlemlol  7525  caucvgprprlemupu  7527  caucvgprprlemexbt  7533  caucvgprprlem1  7536  caucvgprprlem2  7537  suplocexprlemrl  7544  suplocexprlemru  7546  suplocexprlemdisj  7547  suplocexprlemub  7550  suplocexprlemlub  7551  ltsrprg  7574  gt0srpr  7575  recexgt0sr  7600  addgt0sr  7602  mulgt0sr  7605  map2psrprg  7632  suplocsrlemb  7633  suplocsrlem  7635  nnindnn  7720  axcaucvglemcau  7725  axpre-suploclemres  7728  apreap  8368  apreim  8384  mulge0  8400  apti  8403  mulap0bbd  8440  lble  8724  nnind  8755  recnz  9163  uzind  9181  eluzadd  9373  eluzsub  9374  ixxss1  9710  ixxss2  9711  ixxss12  9712  iccss2  9750  iccssioo2  9752  iccssico2  9753  elfzolt2  9957  ioom  10062  flqltp1  10076  addmodlteq  10195  expcl2lemap  10329  expap0i  10349  hashennnuni  10549  crre  10653  caucvgre  10777  cvg1nlemcau  10780  cvg1nlemres  10781  resqrexlemoverl  10817  sqrtge0  10829  fimaxre2  11022  climi  11080  reccn2ap  11106  climge0  11118  nnf1o  11169  sumpr  11206  fsump1i  11226  fsum00  11255  fsumparts  11263  mertenslemi1  11328  addsin  11472  subsin  11473  addcos  11476  subcos  11477  sinbnd2  11484  cosbnd2  11485  evenelz  11587  4dvdseven  11637  infssuzcldc  11667  gcd0id  11690  gcd1  11698  bezoutlemstep  11708  dvdsgcdb  11724  mulgcd  11727  gcdzeq  11733  dvdsmulgcd  11736  sqgcd  11740  dvdssqlem  11741  bezoutr  11743  lcmval  11767  lcmcllem  11771  lcmgcdlem  11781  lcmdvds  11783  lcmgcdeq  11787  lcmdvdsb  11788  mulgcddvds  11798  rpmulgcd2  11799  qredeu  11801  rpdvds  11803  divgcdcoprm0  11805  isprm3  11822  divgcdodd  11844  coprm  11845  rpexp  11854  sqrt2irr  11863  qdencl  11890  qeqnumdivden  11895  divnumden  11897  divdenle  11898  densq  11905  phimullem  11924  hashgcdeq  11927  ennnfonelemom  11944  ennnfonelemex  11950  ennnfonelemf1  11954  ctiunctlemu1st  11970  ctiunctlemu2nd  11971  inopn  12196  restbasg  12363  ssrest  12377  cntop2  12397  icnpimaex  12406  cnima  12415  lmfss  12439  lmtopcnp  12445  txhmeo  12514  txswaphmeo  12516  psmet0  12522  psmettri2  12523  blhalf  12603  bdxmet  12696  xmetxpbl  12703  ioo2bl  12738  tgioo  12741  cncfi  12760  rescncf  12763  cdivcncfap  12782  cnopnap  12789  dedekindeulemeu  12795  dedekindicclemeu  12804  ivthinclemum  12808  ivthinclemlopn  12809  ivthinclemuopn  12811  ivthinclemdisj  12813  ivthdec  12817  limcimo  12829  cnplimcim  12831  cnplimclemr  12833  cnlimci  12837  limccnpcntop  12839  limccnp2lem  12840  limccnp2cntop  12841  limccoap  12842  reldvg  12843  dvbsssg  12850  dvfgg  12852  dvaddxxbr  12860  dvmulxxbr  12861  dvcoapbr  12866  dvcjbr  12867  dvrecap  12872  sin0pilem1  12896  sin0pilem2  12897  tanrpcl  12952  tangtx  12953  cos0pilt1  12967  bj-inf2vnlem1  13312  pwf1oexmid  13340  subctctexmid  13342  iooref1o  13399  taupi  13403  alsi2d  13412  alsc2d  13414
  Copyright terms: Public domain W3C validator