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  6416  nqnq0pi  6420  elnp1st2nd  6458  prcunqu  6467  prnmaxl  6470  prloc  6473  genpcuu  6502  addnqprllem  6509  addlocprlemeq  6515  addlocprlemgt  6516  addlocpr  6518  nqprxx  6528  gtnqex  6531  appdivnq  6543  prmuloclemcalc  6545  prmuloc  6546  mullocprlem  6550  ltprordil  6564  ltexprlemm  6573  ltexprlemopl  6574  ltexprlemlol  6575  ltexprlemopu  6576  ltexprlemupu  6577  ltexprlemdisj  6579  ltexprlemloc  6580  ltexprlemfl  6582  ltexprlemrl  6583  ltexprlemfu  6584  ltexprlemru  6585  ltexpri  6586  recexprlemell  6593  recexprlemelu  6594  recexprlemloc  6602  recexprlempr  6603  recexprlem1ssl  6604  recexprlem1ssu  6605  recexprlemss1l  6606  aptipr  6612  cauappcvgprlemlol  6618  cauappcvgprlemupu  6620  cauappcvgprlemladdfu  6625  cauappcvgprlemladdfl  6626  cauappcvgprlemladdrl  6628  ltsrprg  6655  gt0srpr  6656  recexgt0sr  6681  addgt0sr  6683  mulgt0sr  6684  apreap  7351  apreim  7367  mulge0  7383  apti  7386  mulap0bbd  7403  nnind  7691  recnz  8089  uzind  8105  eluzadd  8257  eluzsub  8258  ixxss1  8523  ixxss2  8524  ixxss12  8525  iccss2  8563  iccssioo2  8565  iccssico2  8566  elfzolt2  8762  expcl2lemap  8901  expap0i  8921  crre  9065  bj-inf2vnlem1  9400  alsi2d  9425  alsc2d  9427
  Copyright terms: Public domain W3C validator