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  3964  potr  4035  brrelex2  4325  feu  5013  fcnvres  5014  fun11iun  5088  elmpt2cl2  5639  tfrlem1  5861  tfrlemisucfn  5876  tfrlemisucaccv  5877  tfrlemibxssdm  5879  tfrlemibfn  5880  tfrlemi14d  5885  swoer  6063  indpi  6319  dfplpq2  6331  ltbtwnnq  6392  enq0tr  6409  nqnq0pi  6413  elnp1st2nd  6451  prcunqu  6460  prnmaxl  6463  prloc  6466  genpcuu  6496  addnqprllem  6503  addlocprlemeq  6509  addlocprlemgt  6510  addlocpr  6512  nqprlu  6522  gtnqex  6524  appdivnq  6534  prmuloclemcalc  6536  prmuloc  6537  mullocprlem  6541  ltprordil  6555  ltexprlemm  6564  ltexprlemopl  6565  ltexprlemlol  6566  ltexprlemopu  6567  ltexprlemupu  6568  ltexprlemdisj  6570  ltexprlemloc  6571  ltexprlemfl  6573  ltexprlemrl  6574  ltexprlemfu  6575  ltexprlemru  6576  ltexpri  6577  recexprlemell  6584  recexprlemelu  6585  recexprlemloc  6593  recexprlempr  6594  recexprlem1ssl  6595  recexprlem1ssu  6596  recexprlemss1l  6597  aptipr  6603  ltsrprg  6627  gt0srpr  6628  recexgt0sr  6653  addgt0sr  6655  mulgt0sr  6656  apreap  7323  apreim  7339  mulge0  7355  apti  7358  mulap0bbd  7375  nnind  7662  recnz  8058  uzind  8074  eluzadd  8226  eluzsub  8227  ixxss1  8491  ixxss2  8492  ixxss12  8493  iccss2  8531  iccssioo2  8533  iccssico2  8534  elfzolt2  8728  bj-inf2vnlem1  9019  alsi2d  9044  alsc2d  9046
  Copyright terms: Public domain W3C validator