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  270  simprbda  378  simp1  964  eldifad  3050  unssad  3221  opth1  4126  opth  4127  0nelop  4138  epelg  4180  poirr  4197  brrelex1  4546  brrelex  4547  asymref  4892  soirri  4901  sotri  4902  fcnvres  5274  fun11iun  5354  elmpocl1  5935  f1od  5939  f1o2d  5941  oprssdmm  6035  smoiso  6165  tfrlem1  6171  swoer  6423  ecopovtrn  6492  ecopovtrng  6495  elmapssres  6533  pmresg  6536  mapsspm  6542  en1uniel  6664  xpf1o  6704  sbthlemi9  6819  supelti  6855  supsnti  6858  supisoti  6863  ctssdccl  6962  ctfoex  6969  fodjum  6984  en2eleq  7015  djuen  7031  ccfunen  7043  dfplpq2  7126  ltbtwnnqq  7187  enq0tr  7206  elnp1st2nd  7248  prcdnql  7256  prnminu  7261  prloc  7263  genpcdl  7291  addnqprulem  7300  addlocprlemlt  7303  addlocprlemgt  7306  addlocprlem  7307  addlocpr  7308  nqprxx  7318  ltnqex  7321  addnqprlemfl  7331  addnqprlemfu  7332  appdivnq  7335  prmuloclemcalc  7337  prmuloc  7338  mullocprlem  7342  mulnqprlemfl  7347  mulnqprlemfu  7348  ltprordil  7361  ltnqpri  7366  ltexprlemm  7372  ltexprlemopl  7373  ltexprlemlol  7374  ltexprlemopu  7375  ltexprlemupu  7376  ltexprlemdisj  7378  ltexprlemloc  7379  ltexprlemfl  7381  ltexprlemrl  7382  ltexprlemfu  7383  ltexprlemru  7384  ltexpri  7385  lteupri  7389  ltaprlem  7390  recexprlemell  7394  recexprlemelu  7395  recexprlemloc  7403  recexprlempr  7404  recexprlem1ssl  7405  recexprlem1ssu  7406  recexprlemss1u  7408  aptipr  7413  cauappcvgprlemm  7417  cauappcvgprlemlol  7419  cauappcvgprlemladdfu  7426  cauappcvgprlemladdfl  7427  cauappcvgprlemladdru  7428  cauappcvgprlem1  7431  caucvgprlemnkj  7438  caucvgprlemnbj  7439  caucvgprlemm  7440  caucvgprlemlol  7442  caucvgprlemladdfu  7449  caucvgprprlemloccalc  7456  caucvgprprlemnkltj  7461  caucvgprprlemnbj  7465  caucvgprprlemml  7466  caucvgprprlemlol  7470  caucvgprprlemloc  7475  caucvgprprlemexbt  7478  suplocexprlemss  7487  suplocexprlemru  7491  suplocexprlemlub  7496  ltsrprg  7519  caucvgsrlemasr  7562  suplocsrlemb  7578  suplocsrlem  7580  suplocsr  7581  axcaucvglemcau  7670  axpre-suploclemres  7673  negf1o  8108  apreap  8312  apreim  8328  msqge0  8341  mulge0  8344  apti  8347  apsscn  8371  mulap0bad  8380  divadddivap  8447  recnz  9095  lbzbi  9357  xadd4d  9608  ixxss1  9627  ixxss2  9628  ixxss12  9629  iccss2  9667  iccssioo2  9669  iccssico2  9670  elfzole1  9872  ioom  9978  flqle  9991  flqltnz  10000  addmodlteq  10111  expclzap  10258  hashennnuni  10465  zfz1isolem1  10523  recl  10565  cvg1nlemcau  10696  cvg1nlemres  10697  resqrtth  10743  fimaxre2  10938  climcl  10991  reccn2ap  11022  isummolemnm  11088  summodclem3  11089  sumpr  11122  fsump1i  11142  fisumcom2  11147  fsum00  11171  fsumparts  11179  mertenslemi1  11244  addsin  11348  subsin  11349  addcos  11352  subcos  11353  sinbnd2  11360  cosbnd2  11361  sin01gt0  11367  cos01gt0  11368  divgcdz  11556  divgcdnn  11559  gcdaddm  11568  bezoutlemstep  11581  dvdsgcdb  11597  dfgcd2  11598  mulgcd  11600  gcdzeq  11606  dvdsmulgcd  11609  sqgcd  11613  bezoutr  11616  lcmval  11640  lcmcllem  11644  gcddvdslcm  11650  lcmgcdlem  11654  lcmgcd  11655  lcmgcdeq  11660  lcmdvdsb  11661  mulgcddvds  11671  rpmulgcd2  11672  qredeu  11674  rpdvds  11676  isprm3  11695  divgcdodd  11717  coprm  11718  rpexp  11727  sqrt2irr  11736  qnumcl  11761  qnumdencoprm  11766  divnumden  11769  numsq  11776  phimullem  11796  hashgcdlem  11798  ennnfonelemg  11811  ennnfonelemf1  11826  ctiunctlemu1st  11842  uniopn  12063  restbasg  12232  cntop1  12265  cnf  12268  cnpf2  12271  lmtopcnp  12314  psmetdmdm  12388  psmetf  12389  psmet0  12391  xmetf  12414  metf  12415  blhalf  12472  xmetxpbl  12572  ioo2bl  12607  tgioo  12610  cncff  12628  rescncf  12632  cdivcncfap  12651  cnopnap  12658  dedekindeulemeu  12664  dedekindicclemeu  12673  limcimolemlt  12685  limcimo  12686  limccnpcntop  12696  limccnp2lem  12697  limccnp2cntop  12698  limccoap  12699  eldvap  12703  dvbsssg  12707  dvfgg  12709  dvaddxxbr  12717  dvmulxxbr  12718  dvcoapbr  12723  dvcj  12725  dvfre  12726  dvrecap  12729  nninfalllem1  13014  alsi1d  13057  alsc1d  13059
  Copyright terms: Public domain W3C validator