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

Theorem simprd 107
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 103 . 2 ((𝜓𝜒) → 𝜒)
31, 2syl 14 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 100
This theorem is referenced by:  bi2  121  simprbi  260  simplbda  366  simp2  905  simp3  906  sbh  1659  eldifbd  2930  unssbd  3121  opth  3974  potr  4045  frind  4089  brrelex2  4383  feu  5072  fcnvres  5073  fun11iun  5147  elmpt2cl2  5700  tfrlem1  5923  tfrlemisucfn  5938  tfrlemisucaccv  5939  tfrlemibxssdm  5941  tfrlemibfn  5942  tfrlemi14d  5947  swoer  6134  cardcl  6359  isnumi  6360  cardval3ex  6363  indpi  6438  dfplpq2  6450  ltbtwnnq  6512  enq0tr  6530  nqnq0pi  6534  elnp1st2nd  6572  prcunqu  6581  prnmaxl  6584  prloc  6587  genpcuu  6616  addnqprllem  6623  addlocprlemeq  6629  addlocprlemgt  6630  addlocpr  6632  nqprxx  6642  gtnqex  6646  appdivnq  6659  prmuloclemcalc  6661  prmuloc  6662  mullocprlem  6666  ltprordil  6685  ltnqpri  6690  ltexprlemm  6696  ltexprlemopl  6697  ltexprlemlol  6698  ltexprlemopu  6699  ltexprlemupu  6700  ltexprlemdisj  6702  ltexprlemloc  6703  ltexprlemfl  6705  ltexprlemrl  6706  ltexprlemfu  6707  ltexprlemru  6708  ltexpri  6709  recexprlemell  6718  recexprlemelu  6719  recexprlemloc  6727  recexprlempr  6728  recexprlem1ssl  6729  recexprlem1ssu  6730  recexprlemss1l  6731  aptipr  6737  cauappcvgprlemlol  6743  cauappcvgprlemupu  6745  cauappcvgprlemladdfu  6750  cauappcvgprlemladdfl  6751  cauappcvgprlemladdrl  6753  caucvgprlemnkj  6762  caucvgprlemnbj  6763  caucvgprlemlol  6766  caucvgprlemupu  6768  caucvgprlemladdfu  6773  caucvgprlem1  6775  caucvgprlem2  6776  caucvgprprlemnjltk  6787  caucvgprprlemnbj  6789  caucvgprprlemlol  6794  caucvgprprlemupu  6796  caucvgprprlemexbt  6802  caucvgprprlem1  6805  caucvgprprlem2  6806  ltsrprg  6830  gt0srpr  6831  recexgt0sr  6856  addgt0sr  6858  mulgt0sr  6860  nnindnn  6965  axcaucvglemcau  6970  apreap  7576  apreim  7592  mulge0  7608  apti  7611  mulap0bbd  7639  nnind  7928  recnz  8331  uzind  8347  eluzadd  8499  eluzsub  8500  ixxss1  8771  ixxss2  8772  ixxss12  8773  iccss2  8811  iccssioo2  8813  iccssico2  8814  elfzolt2  9010  flqltp1  9119  expcl2lemap  9265  expap0i  9285  crre  9455  caucvgre  9578  cvg1nlemcau  9581  cvg1nlemres  9582  resqrexlemoverl  9617  sqrtge0  9629  climi  9806  climge0  9843  sqrt2irr  9876  bj-inf2vnlem1  10093  alsi2d  10118  alsc2d  10120
  Copyright terms: Public domain W3C validator