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

Theorem simpld 111
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 108 . 2  |-  ( ( ps  /\  ch )  ->  ps )
31, 2syl 14 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem is referenced by:  bi1  117  simplbi  272  simprbda  380  simp1  966  eldifad  3052  unssad  3223  opth1  4128  opth  4129  0nelop  4140  epelg  4182  poirr  4199  brrelex1  4548  brrelex  4549  asymref  4894  soirri  4903  sotri  4904  fcnvres  5276  fun11iun  5356  elmpocl1  5937  f1od  5941  f1o2d  5943  oprssdmm  6037  smoiso  6167  tfrlem1  6173  swoer  6425  ecopovtrn  6494  ecopovtrng  6497  elmapssres  6535  pmresg  6538  mapsspm  6544  en1uniel  6666  xpf1o  6706  sbthlemi9  6821  supelti  6857  supsnti  6860  supisoti  6865  ctssdccl  6964  ctfoex  6971  fodjum  6986  en2eleq  7019  djuen  7035  ccfunen  7047  dfplpq2  7130  ltbtwnnqq  7191  enq0tr  7210  elnp1st2nd  7252  prcdnql  7260  prnminu  7265  prloc  7267  genpcdl  7295  addnqprulem  7304  addlocprlemlt  7307  addlocprlemgt  7310  addlocprlem  7311  addlocpr  7312  nqprxx  7322  ltnqex  7325  addnqprlemfl  7335  addnqprlemfu  7336  appdivnq  7339  prmuloclemcalc  7341  prmuloc  7342  mullocprlem  7346  mulnqprlemfl  7351  mulnqprlemfu  7352  ltprordil  7365  ltnqpri  7370  ltexprlemm  7376  ltexprlemopl  7377  ltexprlemlol  7378  ltexprlemopu  7379  ltexprlemupu  7380  ltexprlemdisj  7382  ltexprlemloc  7383  ltexprlemfl  7385  ltexprlemrl  7386  ltexprlemfu  7387  ltexprlemru  7388  ltexpri  7389  lteupri  7393  ltaprlem  7394  recexprlemell  7398  recexprlemelu  7399  recexprlemloc  7407  recexprlempr  7408  recexprlem1ssl  7409  recexprlem1ssu  7410  recexprlemss1u  7412  aptipr  7417  cauappcvgprlemm  7421  cauappcvgprlemlol  7423  cauappcvgprlemladdfu  7430  cauappcvgprlemladdfl  7431  cauappcvgprlemladdru  7432  cauappcvgprlem1  7435  caucvgprlemnkj  7442  caucvgprlemnbj  7443  caucvgprlemm  7444  caucvgprlemlol  7446  caucvgprlemladdfu  7453  caucvgprprlemloccalc  7460  caucvgprprlemnkltj  7465  caucvgprprlemnbj  7469  caucvgprprlemml  7470  caucvgprprlemlol  7474  caucvgprprlemloc  7479  caucvgprprlemexbt  7482  suplocexprlemss  7491  suplocexprlemru  7495  suplocexprlemlub  7500  ltsrprg  7523  caucvgsrlemasr  7566  suplocsrlemb  7582  suplocsrlem  7584  suplocsr  7585  axcaucvglemcau  7674  axpre-suploclemres  7677  negf1o  8112  apreap  8317  apreim  8333  msqge0  8346  mulge0  8349  apti  8352  apsscn  8377  mulap0bad  8388  divadddivap  8455  recnz  9112  lbzbi  9376  xadd4d  9636  ixxss1  9655  ixxss2  9656  ixxss12  9657  iccss2  9695  iccssioo2  9697  iccssico2  9698  elfzole1  9900  ioom  10006  flqle  10019  flqltnz  10028  addmodlteq  10139  expclzap  10286  hashennnuni  10493  zfz1isolem1  10551  recl  10593  cvg1nlemcau  10724  cvg1nlemres  10725  resqrtth  10771  fimaxre2  10966  climcl  11019  reccn2ap  11050  isummolemnm  11116  summodclem3  11117  sumpr  11150  fsump1i  11170  fisumcom2  11175  fsum00  11199  fsumparts  11207  mertenslemi1  11272  addsin  11376  subsin  11377  addcos  11380  subcos  11381  sinbnd2  11388  cosbnd2  11389  sin01gt0  11395  cos01gt0  11396  divgcdz  11587  divgcdnn  11590  gcdaddm  11599  bezoutlemstep  11612  dvdsgcdb  11628  dfgcd2  11629  mulgcd  11631  gcdzeq  11637  dvdsmulgcd  11640  sqgcd  11644  bezoutr  11647  lcmval  11671  lcmcllem  11675  gcddvdslcm  11681  lcmgcdlem  11685  lcmgcd  11686  lcmgcdeq  11691  lcmdvdsb  11692  mulgcddvds  11702  rpmulgcd2  11703  qredeu  11705  rpdvds  11707  isprm3  11726  divgcdodd  11748  coprm  11749  rpexp  11758  sqrt2irr  11767  qnumcl  11793  qnumdencoprm  11798  divnumden  11801  numsq  11808  phimullem  11828  hashgcdlem  11830  ennnfonelemg  11843  ennnfonelemf1  11858  ctiunctlemu1st  11874  uniopn  12095  restbasg  12264  cntop1  12297  cnf  12300  cnpf2  12303  lmtopcnp  12346  psmetdmdm  12420  psmetf  12421  psmet0  12423  xmetf  12446  metf  12447  blhalf  12504  xmetxpbl  12604  ioo2bl  12639  tgioo  12642  cncff  12660  rescncf  12664  cdivcncfap  12683  cnopnap  12690  dedekindeulemeu  12696  dedekindicclemeu  12705  ivthinclemlm  12708  ivthinclemlopn  12710  ivthinclemuopn  12712  ivthinclemdisj  12714  ivthdec  12718  limcimolemlt  12729  limcimo  12730  limccnpcntop  12740  limccnp2lem  12741  limccnp2cntop  12742  limccoap  12743  eldvap  12747  dvbsssg  12751  dvfgg  12753  dvaddxxbr  12761  dvmulxxbr  12762  dvcoapbr  12767  dvcj  12769  dvfre  12770  dvrecap  12773  sin0pilem1  12789  sin0pilem2  12790  pilem3  12791  tanrpcl  12845  tangtx  12846  nninfalllem1  13130  alsi1d  13174  alsc1d  13176
  Copyright terms: Public domain W3C validator