ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  simprd Structured version   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  904  simp3  905  sbh  1656  eldifbd  2924  unssbd  3115  opth  3965  potr  4036  brrelex2  4326  feu  5015  fcnvres  5016  fun11iun  5090  elmpt2cl2  5642  tfrlem1  5864  tfrlemisucfn  5879  tfrlemisucaccv  5880  tfrlemibxssdm  5882  tfrlemibfn  5883  tfrlemi14d  5888  swoer  6070  indpi  6326  dfplpq2  6338  ltbtwnnq  6399  enq0tr  6417  nqnq0pi  6421  elnp1st2nd  6459  prcunqu  6468  prnmaxl  6471  prloc  6474  genpcuu  6503  addnqprllem  6510  addlocprlemeq  6516  addlocprlemgt  6517  addlocpr  6519  nqprxx  6529  gtnqex  6532  appdivnq  6544  prmuloclemcalc  6546  prmuloc  6547  mullocprlem  6551  ltprordil  6565  ltexprlemm  6574  ltexprlemopl  6575  ltexprlemlol  6576  ltexprlemopu  6577  ltexprlemupu  6578  ltexprlemdisj  6580  ltexprlemloc  6581  ltexprlemfl  6583  ltexprlemrl  6584  ltexprlemfu  6585  ltexprlemru  6586  ltexpri  6587  recexprlemell  6594  recexprlemelu  6595  recexprlemloc  6603  recexprlempr  6604  recexprlem1ssl  6605  recexprlem1ssu  6606  recexprlemss1l  6607  aptipr  6613  cauappcvgprlemlol  6619  cauappcvgprlemupu  6621  cauappcvgprlemladdfu  6626  cauappcvgprlemladdfl  6627  cauappcvgprlemladdrl  6629  caucvgprlemnkj  6637  caucvgprlemnbj  6638  caucvgprlemlol  6641  caucvgprlemupu  6643  caucvgprlemladdfu  6648  caucvgprlem1  6650  caucvgprlem2  6651  ltsrprg  6675  gt0srpr  6676  recexgt0sr  6701  addgt0sr  6703  mulgt0sr  6704  apreap  7371  apreim  7387  mulge0  7403  apti  7406  mulap0bbd  7423  nnind  7711  recnz  8109  uzind  8125  eluzadd  8277  eluzsub  8278  ixxss1  8543  ixxss2  8544  ixxss12  8545  iccss2  8583  iccssioo2  8585  iccssico2  8586  elfzolt2  8782  expcl2lemap  8921  expap0i  8941  crre  9085  bj-inf2vnlem1  9430  alsi2d  9455  alsc2d  9457
  Copyright terms: Public domain W3C validator