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

Theorem simpld 109
Description: Deduction eliminating a conjunct. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
simpld.1  |-  ( ph  ->  ( ps  /\  ch ) )
Assertion
Ref Expression
simpld  |-  ( ph  ->  ps )

Proof of Theorem simpld
StepHypRef Expression
1 simpld.1 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
2 simpl 106 . 2  |-  ( ( ps  /\  ch )  ->  ps )
31, 2syl 14 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103
This theorem is referenced by:  bi1  115  simplbi  263  simprbda  369  simp1  915  eldifad  2957  unssad  3148  opth1  4001  opth  4002  0nelop  4013  epelg  4055  poirr  4072  brrelex  4410  asymref  4738  soirri  4747  sotri  4748  fcnvres  5101  fun11iun  5175  elmpt2cl1  5727  f1od  5731  f1o2d  5733  smoiso  5948  tfrlem1  5954  swoer  6165  ecopovtrn  6234  ecopovtrng  6237  en1uniel  6315  supsnti  6409  supisoti  6414  dfplpq2  6510  ltbtwnnqq  6571  enq0tr  6590  elnp1st2nd  6632  prcdnql  6640  prnminu  6645  prloc  6647  genpcdl  6675  addnqprulem  6684  addlocprlemlt  6687  addlocprlemgt  6690  addlocprlem  6691  addlocpr  6692  nqprxx  6702  ltnqex  6705  addnqprlemfl  6715  addnqprlemfu  6716  appdivnq  6719  prmuloclemcalc  6721  prmuloc  6722  mullocprlem  6726  mulnqprlemfl  6731  mulnqprlemfu  6732  ltprordil  6745  ltnqpri  6750  ltexprlemm  6756  ltexprlemopl  6757  ltexprlemlol  6758  ltexprlemopu  6759  ltexprlemupu  6760  ltexprlemdisj  6762  ltexprlemloc  6763  ltexprlemfl  6765  ltexprlemrl  6766  ltexprlemfu  6767  ltexprlemru  6768  ltexpri  6769  lteupri  6773  ltaprlem  6774  recexprlemell  6778  recexprlemelu  6779  recexprlemloc  6787  recexprlempr  6788  recexprlem1ssl  6789  recexprlem1ssu  6790  recexprlemss1u  6792  aptipr  6797  cauappcvgprlemm  6801  cauappcvgprlemlol  6803  cauappcvgprlemladdfu  6810  cauappcvgprlemladdfl  6811  cauappcvgprlemladdru  6812  cauappcvgprlem1  6815  caucvgprlemnkj  6822  caucvgprlemnbj  6823  caucvgprlemm  6824  caucvgprlemlol  6826  caucvgprlemladdfu  6833  caucvgprprlemloccalc  6840  caucvgprprlemnkltj  6845  caucvgprprlemnbj  6849  caucvgprprlemml  6850  caucvgprprlemlol  6854  caucvgprprlemloc  6859  caucvgprprlemexbt  6862  ltsrprg  6890  caucvgsrlemasr  6932  axcaucvglemcau  7030  apreap  7652  apreim  7668  msqge0  7681  mulge0  7684  apti  7687  mulap0bad  7714  divadddivap  7778  recnz  8391  lbzbi  8648  ixxss1  8874  ixxss2  8875  ixxss12  8876  iccss2  8914  iccssioo2  8916  iccssico2  8917  elfzole1  9113  ioom  9217  flqle  9228  flqltnz  9237  addmodlteq  9348  expclzap  9445  recl  9681  cvg1nlemcau  9811  cvg1nlemres  9812  resqrtth  9858  climcl  10034  sqrt2irr  10251  alsi1d  10507  alsc1d  10509
  Copyright terms: Public domain W3C validator