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  3963  opth  3964  0nelop  3975  epelg  4017  poirr  4034  brrelex  4324  asymref  4652  soirri  4661  sotri  4662  fcnvres  5014  fun11iun  5088  elmpt2cl1  5638  f1od  5642  f1o2d  5644  smoiso  5855  tfrlem1  5861  swoer  6063  ecopovtrn  6132  ecopovtrng  6135  en1uniel  6213  dfplpq2  6331  ltbtwnnqq  6391  enq0tr  6409  elnp1st2nd  6451  prcdnql  6459  prnminu  6464  prloc  6466  genpcdl  6495  addnqprulem  6504  addlocprlemlt  6507  addlocprlemgt  6510  addlocprlem  6511  addlocpr  6512  nqprlu  6522  ltnqex  6523  addnqpr1lemil  6531  addnqpr1lemiu  6532  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  ltaprlem  6581  recexprlemell  6584  recexprlemelu  6585  recexprlemloc  6593  recexprlempr  6594  recexprlem1ssl  6595  recexprlem1ssu  6596  recexprlemss1u  6598  aptipr  6603  ltsrprg  6627  apreap  7323  apreim  7339  msqge0  7352  mulge0  7355  apti  7358  mulap0bad  7374  divadddivap  7437  recnz  8058  lbzbi  8276  ixxss1  8491  ixxss2  8492  ixxss12  8493  iccss2  8531  iccssioo2  8533  iccssico2  8534  elfzole1  8727  alsi1d  9043  alsc1d  9045
  Copyright terms: Public domain W3C validator