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

Theorem simprd 112
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 108 . 2 ((𝜓𝜒) → 𝜒)
31, 2syl 14 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-ia2 105
This theorem is referenced by:  bi2  128  simprbi  269  simplbda  376  simp2  942  simp3  943  sbh  1703  eldifbd  3000  unssbd  3167  opth  4040  potr  4111  frind  4155  brrelex2  4451  funinsn  5030  feu  5158  fcnvres  5159  fun11iun  5239  elmpt2cl2  5803  tfrlem1  6029  tfrlemisucfn  6045  tfrlemisucaccv  6046  tfrlemibxssdm  6048  tfrlemibfn  6049  tfrlemi14d  6054  swoer  6274  elmapssres  6384  mapsspm  6393  pmsspw  6394  mapss  6402  dom0  6508  xpf1o  6514  sbthlemi8  6620  sbthlemi9  6621  supelti  6644  supisoti  6652  djulclb  6694  cardcl  6756  isnumi  6757  cardval3ex  6760  en2eleq  6768  indpi  6848  dfplpq2  6860  ltbtwnnq  6922  enq0tr  6940  nqnq0pi  6944  elnp1st2nd  6982  prcunqu  6991  prnmaxl  6994  prloc  6997  genpcuu  7026  addnqprllem  7033  addlocprlemeq  7039  addlocprlemgt  7040  addlocpr  7042  nqprxx  7052  gtnqex  7056  appdivnq  7069  prmuloclemcalc  7071  prmuloc  7072  mullocprlem  7076  ltprordil  7095  ltnqpri  7100  ltexprlemm  7106  ltexprlemopl  7107  ltexprlemlol  7108  ltexprlemopu  7109  ltexprlemupu  7110  ltexprlemdisj  7112  ltexprlemloc  7113  ltexprlemfl  7115  ltexprlemrl  7116  ltexprlemfu  7117  ltexprlemru  7118  ltexpri  7119  recexprlemell  7128  recexprlemelu  7129  recexprlemloc  7137  recexprlempr  7138  recexprlem1ssl  7139  recexprlem1ssu  7140  recexprlemss1l  7141  aptipr  7147  cauappcvgprlemlol  7153  cauappcvgprlemupu  7155  cauappcvgprlemladdfu  7160  cauappcvgprlemladdfl  7161  cauappcvgprlemladdrl  7163  caucvgprlemnkj  7172  caucvgprlemnbj  7173  caucvgprlemlol  7176  caucvgprlemupu  7178  caucvgprlemladdfu  7183  caucvgprlem1  7185  caucvgprlem2  7186  caucvgprprlemnjltk  7197  caucvgprprlemnbj  7199  caucvgprprlemlol  7204  caucvgprprlemupu  7206  caucvgprprlemexbt  7212  caucvgprprlem1  7215  caucvgprprlem2  7216  ltsrprg  7240  gt0srpr  7241  recexgt0sr  7266  addgt0sr  7268  mulgt0sr  7270  nnindnn  7375  axcaucvglemcau  7380  apreap  8008  apreim  8024  mulge0  8040  apti  8043  mulap0bbd  8071  lble  8346  nnind  8376  recnz  8775  uzind  8793  eluzadd  8982  eluzsub  8983  ixxss1  9257  ixxss2  9258  ixxss12  9259  iccss2  9297  iccssioo2  9299  iccssico2  9300  elfzolt2  9498  ioom  9603  flqltp1  9617  addmodlteq  9736  expcl2lemap  9887  expap0i  9907  hashennnuni  10105  crre  10208  caucvgre  10331  cvg1nlemcau  10334  cvg1nlemres  10335  resqrexlemoverl  10371  sqrtge0  10383  fimaxre2  10574  climi  10591  climge0  10629  isummolemnm  10682  sumpr  10713  evenelz  10792  4dvdseven  10842  infssuzcldc  10872  gcd0id  10895  gcd1  10903  bezoutlemstep  10911  dvdsgcdb  10927  mulgcd  10930  gcdzeq  10936  dvdsmulgcd  10939  sqgcd  10943  dvdssqlem  10944  bezoutr  10946  lcmval  10970  lcmcllem  10974  lcmgcdlem  10984  lcmdvds  10986  lcmgcdeq  10990  lcmdvdsb  10991  mulgcddvds  11001  rpmulgcd2  11002  qredeu  11004  rpdvds  11006  divgcdcoprm0  11008  isprm3  11025  divgcdodd  11047  coprm  11048  rpexp  11057  sqrt2irr  11066  qdencl  11092  qeqnumdivden  11097  divnumden  11099  divdenle  11100  densq  11107  phimullem  11126  hashgcdeq  11129  bj-inf2vnlem1  11353  alsi2d  11411  alsc2d  11413
  Copyright terms: Public domain W3C validator