ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  simprd Unicode 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  |-  ( ph  ->  ( ps  /\  ch ) )
Assertion
Ref Expression
simprd  |-  ( ph  ->  ch )

Proof of Theorem simprd
StepHypRef Expression
1 simprd.1 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
2 simpr 108 . 2  |-  ( ( ps  /\  ch )  ->  ch )
31, 2syl 14 1  |-  ( ph  ->  ch )
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  940  simp3  941  sbh  1700  eldifbd  2986  unssbd  3151  opth  4000  potr  4071  frind  4115  brrelex2  4409  funinsn  4979  feu  5103  fcnvres  5104  fun11iun  5178  elmpt2cl2  5731  tfrlem1  5957  tfrlemisucfn  5973  tfrlemisucaccv  5974  tfrlemibxssdm  5976  tfrlemibfn  5977  tfrlemi14d  5982  swoer  6200  xpf1o  6385  supelti  6474  supisoti  6482  cardcl  6509  isnumi  6510  cardval3ex  6513  en2eleq  6521  indpi  6594  dfplpq2  6606  ltbtwnnq  6668  enq0tr  6686  nqnq0pi  6690  elnp1st2nd  6728  prcunqu  6737  prnmaxl  6740  prloc  6743  genpcuu  6772  addnqprllem  6779  addlocprlemeq  6785  addlocprlemgt  6786  addlocpr  6788  nqprxx  6798  gtnqex  6802  appdivnq  6815  prmuloclemcalc  6817  prmuloc  6818  mullocprlem  6822  ltprordil  6841  ltnqpri  6846  ltexprlemm  6852  ltexprlemopl  6853  ltexprlemlol  6854  ltexprlemopu  6855  ltexprlemupu  6856  ltexprlemdisj  6858  ltexprlemloc  6859  ltexprlemfl  6861  ltexprlemrl  6862  ltexprlemfu  6863  ltexprlemru  6864  ltexpri  6865  recexprlemell  6874  recexprlemelu  6875  recexprlemloc  6883  recexprlempr  6884  recexprlem1ssl  6885  recexprlem1ssu  6886  recexprlemss1l  6887  aptipr  6893  cauappcvgprlemlol  6899  cauappcvgprlemupu  6901  cauappcvgprlemladdfu  6906  cauappcvgprlemladdfl  6907  cauappcvgprlemladdrl  6909  caucvgprlemnkj  6918  caucvgprlemnbj  6919  caucvgprlemlol  6922  caucvgprlemupu  6924  caucvgprlemladdfu  6929  caucvgprlem1  6931  caucvgprlem2  6932  caucvgprprlemnjltk  6943  caucvgprprlemnbj  6945  caucvgprprlemlol  6950  caucvgprprlemupu  6952  caucvgprprlemexbt  6958  caucvgprprlem1  6961  caucvgprprlem2  6962  ltsrprg  6986  gt0srpr  6987  recexgt0sr  7012  addgt0sr  7014  mulgt0sr  7016  nnindnn  7121  axcaucvglemcau  7126  apreap  7754  apreim  7770  mulge0  7786  apti  7789  mulap0bbd  7817  lble  8092  nnind  8122  recnz  8521  uzind  8539  eluzadd  8728  eluzsub  8729  ixxss1  9003  ixxss2  9004  ixxss12  9005  iccss2  9043  iccssioo2  9045  iccssico2  9046  elfzolt2  9242  ioom  9347  flqltp1  9361  addmodlteq  9480  expcl2lemap  9585  expap0i  9605  sizeennnuni  9803  crre  9882  caucvgre  10005  cvg1nlemcau  10008  cvg1nlemres  10009  resqrexlemoverl  10045  sqrtge0  10057  fimaxre2  10247  climi  10264  climge0  10301  evenelz  10411  4dvdseven  10461  infssuzcldc  10491  gcd0id  10514  gcd1  10522  bezoutlemstep  10530  dvdsgcdb  10546  mulgcd  10549  gcdzeq  10555  dvdsmulgcd  10558  sqgcd  10562  dvdssqlem  10563  bezoutr  10565  lcmval  10589  lcmcllem  10593  lcmgcdlem  10603  lcmdvds  10605  lcmgcdeq  10609  lcmdvdsb  10610  mulgcddvds  10620  rpmulgcd2  10621  qredeu  10623  rpdvds  10625  divgcdcoprm0  10627  isprm3  10644  divgcdodd  10666  coprm  10667  rpexp  10676  sqrt2irr  10685  bj-inf2vnlem1  10923  alsi2d  10951  alsc2d  10953
  Copyright terms: Public domain W3C validator