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

Theorem simpld 110
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 107 . 2 ((𝜓𝜒) → 𝜓)
31, 2syl 14 1 (𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem is referenced by:  bi1  116  simplbi  268  simprbda  375  simp1  939  eldifad  2985  unssad  3150  opth1  3999  opth  4000  0nelop  4011  epelg  4053  poirr  4070  brrelex  4408  asymref  4740  soirri  4749  sotri  4750  fcnvres  5104  fun11iun  5178  elmpt2cl1  5730  f1od  5734  f1o2d  5736  smoiso  5951  tfrlem1  5957  swoer  6200  ecopovtrn  6269  ecopovtrng  6272  en1uniel  6351  xpf1o  6385  supelti  6474  supsnti  6477  supisoti  6482  en2eleq  6521  dfplpq2  6606  ltbtwnnqq  6667  enq0tr  6686  elnp1st2nd  6728  prcdnql  6736  prnminu  6741  prloc  6743  genpcdl  6771  addnqprulem  6780  addlocprlemlt  6783  addlocprlemgt  6786  addlocprlem  6787  addlocpr  6788  nqprxx  6798  ltnqex  6801  addnqprlemfl  6811  addnqprlemfu  6812  appdivnq  6815  prmuloclemcalc  6817  prmuloc  6818  mullocprlem  6822  mulnqprlemfl  6827  mulnqprlemfu  6828  ltprordil  6841  ltnqpri  6846  ltexprlemm  6852  ltexprlemopl  6853  ltexprlemlol  6854  ltexprlemopu  6855  ltexprlemupu  6856  ltexprlemdisj  6858  ltexprlemloc  6859  ltexprlemfl  6861  ltexprlemrl  6862  ltexprlemfu  6863  ltexprlemru  6864  ltexpri  6865  lteupri  6869  ltaprlem  6870  recexprlemell  6874  recexprlemelu  6875  recexprlemloc  6883  recexprlempr  6884  recexprlem1ssl  6885  recexprlem1ssu  6886  recexprlemss1u  6888  aptipr  6893  cauappcvgprlemm  6897  cauappcvgprlemlol  6899  cauappcvgprlemladdfu  6906  cauappcvgprlemladdfl  6907  cauappcvgprlemladdru  6908  cauappcvgprlem1  6911  caucvgprlemnkj  6918  caucvgprlemnbj  6919  caucvgprlemm  6920  caucvgprlemlol  6922  caucvgprlemladdfu  6929  caucvgprprlemloccalc  6936  caucvgprprlemnkltj  6941  caucvgprprlemnbj  6945  caucvgprprlemml  6946  caucvgprprlemlol  6950  caucvgprprlemloc  6955  caucvgprprlemexbt  6958  ltsrprg  6986  caucvgsrlemasr  7028  axcaucvglemcau  7126  negf1o  7553  apreap  7754  apreim  7770  msqge0  7783  mulge0  7786  apti  7789  mulap0bad  7816  divadddivap  7882  recnz  8521  lbzbi  8782  ixxss1  9003  ixxss2  9004  ixxss12  9005  iccss2  9043  iccssioo2  9045  iccssico2  9046  elfzole1  9241  ioom  9347  flqle  9360  flqltnz  9369  addmodlteq  9480  expclzap  9598  sizeennnuni  9803  recl  9878  cvg1nlemcau  10008  cvg1nlemres  10009  resqrtth  10055  fimaxre2  10247  climcl  10259  divgcdz  10507  divgcdnn  10510  gcdaddm  10519  bezoutlemstep  10530  dvdsgcdb  10546  dfgcd2  10547  mulgcd  10549  gcdzeq  10555  dvdsmulgcd  10558  sqgcd  10562  bezoutr  10565  lcmval  10589  lcmcllem  10593  gcddvdslcm  10599  lcmgcdlem  10603  lcmgcd  10604  lcmgcdeq  10609  lcmdvdsb  10610  mulgcddvds  10620  rpmulgcd2  10621  qredeu  10623  rpdvds  10625  isprm3  10644  divgcdodd  10666  coprm  10667  rpexp  10676  sqrt2irr  10685  alsi1d  10950  alsc1d  10952
  Copyright terms: Public domain W3C validator