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  967  simp3  968  sbh  1734  eldifbd  3053  unssbd  3224  opth  4129  potr  4200  frind  4244  brrelex2  4550  funinsn  5142  feu  5275  fcnvres  5276  fun11iun  5356  elmpocl2  5938  oprssdmm  6037  tfrlem1  6173  tfrlemisucfn  6189  tfrlemisucaccv  6190  tfrlemibxssdm  6192  tfrlemibfn  6193  tfrlemi14d  6198  swoer  6425  elmapssres  6535  mapsspm  6544  pmsspw  6545  mapss  6553  dom0  6700  xpf1o  6706  sbthlemi8  6820  sbthlemi9  6821  supelti  6857  supisoti  6865  djulclb  6908  cardcl  7005  isnumi  7006  cardval3ex  7009  exmidonfinlem  7017  en2eleq  7019  acfun  7031  exmidaclem  7032  ccfunen  7047  indpi  7118  dfplpq2  7130  ltbtwnnq  7192  enq0tr  7210  nqnq0pi  7214  elnp1st2nd  7252  prcunqu  7261  prnmaxl  7264  prloc  7267  genpcuu  7296  addnqprllem  7303  addlocprlemeq  7309  addlocprlemgt  7310  addlocpr  7312  nqprxx  7322  gtnqex  7326  appdivnq  7339  prmuloclemcalc  7341  prmuloc  7342  mullocprlem  7346  ltprordil  7365  ltnqpri  7370  ltexprlemm  7376  ltexprlemopl  7377  ltexprlemlol  7378  ltexprlemopu  7379  ltexprlemupu  7380  ltexprlemdisj  7382  ltexprlemloc  7383  ltexprlemfl  7385  ltexprlemrl  7386  ltexprlemfu  7387  ltexprlemru  7388  ltexpri  7389  recexprlemell  7398  recexprlemelu  7399  recexprlemloc  7407  recexprlempr  7408  recexprlem1ssl  7409  recexprlem1ssu  7410  recexprlemss1l  7411  aptipr  7417  cauappcvgprlemlol  7423  cauappcvgprlemupu  7425  cauappcvgprlemladdfu  7430  cauappcvgprlemladdfl  7431  cauappcvgprlemladdrl  7433  caucvgprlemnkj  7442  caucvgprlemnbj  7443  caucvgprlemlol  7446  caucvgprlemupu  7448  caucvgprlemladdfu  7453  caucvgprlem1  7455  caucvgprlem2  7456  caucvgprprlemnjltk  7467  caucvgprprlemnbj  7469  caucvgprprlemlol  7474  caucvgprprlemupu  7476  caucvgprprlemexbt  7482  caucvgprprlem1  7485  caucvgprprlem2  7486  suplocexprlemrl  7493  suplocexprlemru  7495  suplocexprlemdisj  7496  suplocexprlemub  7499  suplocexprlemlub  7500  ltsrprg  7523  gt0srpr  7524  recexgt0sr  7549  addgt0sr  7551  mulgt0sr  7554  map2psrprg  7581  suplocsrlemb  7582  suplocsrlem  7584  nnindnn  7669  axcaucvglemcau  7674  axpre-suploclemres  7677  apreap  8317  apreim  8333  mulge0  8349  apti  8352  mulap0bbd  8389  lble  8673  nnind  8704  recnz  9112  uzind  9130  eluzadd  9322  eluzsub  9323  ixxss1  9655  ixxss2  9656  ixxss12  9657  iccss2  9695  iccssioo2  9697  iccssico2  9698  elfzolt2  9901  ioom  10006  flqltp1  10020  addmodlteq  10139  expcl2lemap  10273  expap0i  10293  hashennnuni  10493  crre  10597  caucvgre  10721  cvg1nlemcau  10724  cvg1nlemres  10725  resqrexlemoverl  10761  sqrtge0  10773  fimaxre2  10966  climi  11024  reccn2ap  11050  climge0  11062  isummolemnm  11116  sumpr  11150  fsump1i  11170  fsum00  11199  fsumparts  11207  mertenslemi1  11272  addsin  11376  subsin  11377  addcos  11380  subcos  11381  sinbnd2  11388  cosbnd2  11389  evenelz  11491  4dvdseven  11541  infssuzcldc  11571  gcd0id  11594  gcd1  11602  bezoutlemstep  11612  dvdsgcdb  11628  mulgcd  11631  gcdzeq  11637  dvdsmulgcd  11640  sqgcd  11644  dvdssqlem  11645  bezoutr  11647  lcmval  11671  lcmcllem  11675  lcmgcdlem  11685  lcmdvds  11687  lcmgcdeq  11691  lcmdvdsb  11692  mulgcddvds  11702  rpmulgcd2  11703  qredeu  11705  rpdvds  11707  divgcdcoprm0  11709  isprm3  11726  divgcdodd  11748  coprm  11749  rpexp  11758  sqrt2irr  11767  qdencl  11794  qeqnumdivden  11799  divnumden  11801  divdenle  11802  densq  11809  phimullem  11828  hashgcdeq  11831  ennnfonelemom  11848  ennnfonelemex  11854  ennnfonelemf1  11858  ctiunctlemu1st  11874  ctiunctlemu2nd  11875  inopn  12097  restbasg  12264  ssrest  12278  cntop2  12298  icnpimaex  12307  cnima  12316  lmfss  12340  lmtopcnp  12346  txhmeo  12415  txswaphmeo  12417  psmet0  12423  psmettri2  12424  blhalf  12504  bdxmet  12597  xmetxpbl  12604  ioo2bl  12639  tgioo  12642  cncfi  12661  rescncf  12664  cdivcncfap  12683  cnopnap  12690  dedekindeulemeu  12696  dedekindicclemeu  12705  ivthinclemum  12709  ivthinclemlopn  12710  ivthinclemuopn  12712  ivthinclemdisj  12714  ivthdec  12718  limcimo  12730  cnplimcim  12732  cnplimclemr  12734  cnlimci  12738  limccnpcntop  12740  limccnp2lem  12741  limccnp2cntop  12742  limccoap  12743  reldvg  12744  dvbsssg  12751  dvfgg  12753  dvaddxxbr  12761  dvmulxxbr  12762  dvcoapbr  12767  dvcjbr  12768  dvrecap  12773  sin0pilem1  12789  sin0pilem2  12790  tanrpcl  12845  tangtx  12846  bj-inf2vnlem1  13095  pwf1oexmid  13121  subctctexmid  13123  taupi  13166  alsi2d  13175  alsc2d  13177
  Copyright terms: Public domain W3C validator