ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  simpld 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  904  eldifad  2929  unssad  3120  opth1  3973  opth  3974  0nelop  3985  epelg  4027  poirr  4044  brrelex  4382  asymref  4710  soirri  4719  sotri  4720  fcnvres  5073  fun11iun  5147  elmpt2cl1  5699  f1od  5703  f1o2d  5705  smoiso  5917  tfrlem1  5923  swoer  6134  ecopovtrn  6203  ecopovtrng  6206  en1uniel  6284  dfplpq2  6450  ltbtwnnqq  6511  enq0tr  6530  elnp1st2nd  6572  prcdnql  6580  prnminu  6585  prloc  6587  genpcdl  6615  addnqprulem  6624  addlocprlemlt  6627  addlocprlemgt  6630  addlocprlem  6631  addlocpr  6632  nqprxx  6642  ltnqex  6645  addnqprlemfl  6655  addnqprlemfu  6656  appdivnq  6659  prmuloclemcalc  6661  prmuloc  6662  mullocprlem  6666  mulnqprlemfl  6671  mulnqprlemfu  6672  ltprordil  6685  ltnqpri  6690  ltexprlemm  6696  ltexprlemopl  6697  ltexprlemlol  6698  ltexprlemopu  6699  ltexprlemupu  6700  ltexprlemdisj  6702  ltexprlemloc  6703  ltexprlemfl  6705  ltexprlemrl  6706  ltexprlemfu  6707  ltexprlemru  6708  ltexpri  6709  lteupri  6713  ltaprlem  6714  recexprlemell  6718  recexprlemelu  6719  recexprlemloc  6727  recexprlempr  6728  recexprlem1ssl  6729  recexprlem1ssu  6730  recexprlemss1u  6732  aptipr  6737  cauappcvgprlemm  6741  cauappcvgprlemlol  6743  cauappcvgprlemladdfu  6750  cauappcvgprlemladdfl  6751  cauappcvgprlemladdru  6752  cauappcvgprlem1  6755  caucvgprlemnkj  6762  caucvgprlemnbj  6763  caucvgprlemm  6764  caucvgprlemlol  6766  caucvgprlemladdfu  6773  caucvgprprlemloccalc  6780  caucvgprprlemnkltj  6785  caucvgprprlemnbj  6789  caucvgprprlemml  6790  caucvgprprlemlol  6794  caucvgprprlemloc  6799  caucvgprprlemexbt  6802  ltsrprg  6830  caucvgsrlemasr  6872  axcaucvglemcau  6970  apreap  7576  apreim  7592  msqge0  7605  mulge0  7608  apti  7611  mulap0bad  7638  divadddivap  7701  recnz  8331  lbzbi  8549  ixxss1  8771  ixxss2  8772  ixxss12  8773  iccss2  8811  iccssioo2  8813  iccssico2  8814  elfzole1  9009  flqle  9118  flqltnz  9127  expclzap  9278  recl  9451  cvg1nlemcau  9581  cvg1nlemres  9582  resqrtth  9627  climcl  9801  sqrt2irr  9876  alsi1d  10117  alsc1d  10119
  Copyright terms: Public domain W3C validator