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  6416  elnp1st2nd  6458  prcdnql  6466  prnminu  6471  prloc  6473  genpcdl  6501  addnqprulem  6510  addlocprlemlt  6513  addlocprlemgt  6516  addlocprlem  6517  addlocpr  6518  nqprxx  6528  ltnqex  6530  addnqprlemfl  6539  addnqprlemfu  6540  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  ltaprlem  6590  recexprlemell  6593  recexprlemelu  6594  recexprlemloc  6602  recexprlempr  6603  recexprlem1ssl  6604  recexprlem1ssu  6605  recexprlemss1u  6607  aptipr  6612  cauappcvgprlemm  6616  cauappcvgprlemlol  6618  cauappcvgprlemladdfu  6625  cauappcvgprlemladdfl  6626  cauappcvgprlemladdru  6627  cauappcvgprlem1  6630  ltsrprg  6655  apreap  7351  apreim  7367  msqge0  7380  mulge0  7383  apti  7386  mulap0bad  7402  divadddivap  7465  recnz  8089  lbzbi  8307  ixxss1  8523  ixxss2  8524  ixxss12  8525  iccss2  8563  iccssioo2  8565  iccssico2  8566  elfzole1  8761  expclzap  8914  recl  9061  alsi1d  9424  alsc1d  9426
  Copyright terms: Public domain W3C validator