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

Theorem simpld 105
Description: Deduction eliminating a conjunct. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
simpld.1 (φ → (ψ χ))
Assertion
Ref Expression
simpld (φψ)

Proof of Theorem simpld
StepHypRef Expression
1 simpld.1 . 2 (φ → (ψ χ))
2 simpl 102 . 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-ia1 99
This theorem is referenced by:  bi1  111  simplbi  259  simprbda  365  simp1  903  eldifad  2923  unssad  3114  opth1  3964  opth  3965  0nelop  3976  epelg  4018  poirr  4035  brrelex  4325  asymref  4653  soirri  4662  sotri  4663  fcnvres  5016  fun11iun  5090  elmpt2cl1  5641  f1od  5645  f1o2d  5647  smoiso  5858  tfrlem1  5864  swoer  6070  ecopovtrn  6139  ecopovtrng  6142  en1uniel  6220  dfplpq2  6338  ltbtwnnqq  6398  enq0tr  6417  elnp1st2nd  6459  prcdnql  6467  prnminu  6472  prloc  6474  genpcdl  6502  addnqprulem  6511  addlocprlemlt  6514  addlocprlemgt  6517  addlocprlem  6518  addlocpr  6519  nqprxx  6529  ltnqex  6531  addnqprlemfl  6540  addnqprlemfu  6541  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  ltaprlem  6591  recexprlemell  6594  recexprlemelu  6595  recexprlemloc  6603  recexprlempr  6604  recexprlem1ssl  6605  recexprlem1ssu  6606  recexprlemss1u  6608  aptipr  6613  cauappcvgprlemm  6617  cauappcvgprlemlol  6619  cauappcvgprlemladdfu  6626  cauappcvgprlemladdfl  6627  cauappcvgprlemladdru  6628  cauappcvgprlem1  6631  caucvgprlemnkj  6637  caucvgprlemnbj  6638  caucvgprlemm  6639  caucvgprlemlol  6641  caucvgprlemladdfu  6648  ltsrprg  6675  apreap  7371  apreim  7387  msqge0  7400  mulge0  7403  apti  7406  mulap0bad  7422  divadddivap  7485  recnz  8109  lbzbi  8327  ixxss1  8543  ixxss2  8544  ixxss12  8545  iccss2  8583  iccssioo2  8585  iccssico2  8586  elfzole1  8781  expclzap  8934  recl  9081  alsi1d  9454  alsc1d  9456
  Copyright terms: Public domain W3C validator