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

Theorem simpll 489
Description: Simplification of a conjunction. (Contributed by NM, 18-Mar-2007.)
Assertion
Ref Expression
simpll  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ph )

Proof of Theorem simpll
StepHypRef Expression
1 id 19 . 2  |-  ( ph  ->  ph )
21ad2antrr 465 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ph )
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  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  simp1ll  978  simp2ll  982  simp3ll  986  rmob  2878  prneimg  3573  ordtri2or2exmidlem  4279  onsucelsucexmidlem  4282  poinxp  4437  mpteqb  5289  fvmptt  5290  fcof1  5451  acexmid  5539  grprinvlem  5723  dftpos4  5909  tfrlem3ag  5955  tfrlem3a  5956  tfrlemi1  5977  tfrexlem  5979  nndifsnid  6111  qsel  6214  ecopovsymg  6236  ecopoverg  6238  th3qlem1  6239  fidifsnid  6363  findcard2  6377  findcard2s  6378  findcard2sd  6380  supisolem  6412  dfplpq2  6510  dfmpq2  6511  mulpipqqs  6529  distrnqg  6543  ltexnqq  6564  subhalfnqq  6570  prarloclemarch  6574  nnnq0lem1  6602  distrnq0  6615  npsspw  6627  prarloclemlo  6650  prarloclem3  6653  prarloclemcalc  6658  genplt2i  6666  distrlem1prl  6738  distrlem1pru  6739  distrlem4prl  6740  distrlem4pru  6741  ltprordil  6745  ltexprlemlol  6758  ltexprlemupu  6760  addextpr  6777  recexprlemopl  6781  recexprlemdisj  6786  recexprlem1ssl  6789  aptiprleml  6795  prsrlem1  6885  recexgt0sr  6916  addcnsr  6968  mulcnsr  6969  mulcnsrec  6977  axaddcl  6998  axmulcl  7000  axmulcom  7003  rereceu  7021  cnegexlem1  7249  cnegex  7252  addsub4  7317  le2add  7513  lt2add  7514  lt2sub  7529  le2sub  7530  rereim  7651  apreim  7668  mulreim  7669  addext  7675  mulext  7679  receuap  7724  rec11ap  7761  rec11rap  7762  divdivdivap  7764  ddcanap  7777  divadddivap  7778  divsubdivap  7779  conjmulap  7780  rerecclap  7781  recgt0  7891  prodgt0gt0  7892  prodgt0  7893  prodge0  7895  ltmul12a  7901  lemul12a  7903  lemulge11  7907  lt2mul2div  7920  ltrec  7924  lerec  7925  lt2msq  7927  ltrec1  7929  le2msq  7942  msq11  7943  ledivp1  7944  mulle0r  7985  peano5uzti  8405  eluzuzle  8577  qreccl  8674  xrltso  8818  z2ge  8840  ixxss1  8874  ixxss2  8875  elioc2  8906  divelunit  8971  fzass4  9027  fzrev  9048  fzonmapblen  9145  elfzodifsumelfzo  9159  ssfzo12bi  9183  qbtwnzlemstep  9205  qbtwnzlemex  9207  rebtwn2z  9211  qbtwnxr  9214  modqid  9299  modqcyc  9309  modqaddabs  9312  modqaddmod  9313  mulqaddmodid  9314  modqadd2mod  9324  modqltm1p1mod  9326  modqsubmod  9332  modqsubmodmod  9333  modqmulmod  9339  modqmulmodr  9340  modqsubdir  9343  expivallem  9421  expp1  9427  expcl2lemap  9432  expnegzap  9454  expadd  9462  expmul  9465  leexp1a  9475  expnlbnd  9541  nn0opth2  9592  bcval  9617  ibcval5  9631  bcpasc  9634  shftfvalg  9647  shftfval  9650  caucvgrelemrec  9806  resqrexlemdecn  9839  sqrtmul  9862  sqrtdiv  9869  leabs  9901  absexpzap  9907  ltabs  9914  abslt  9915  absle  9916  abssubap0  9917  amgm2  9945  icodiamlt  10007  qdenre  10029  climuni  10045  cn1lem  10065  iiserex  10090  iserile  10093  climcau  10097  dvds2ln  10140  dvdsle  10156  divconjdvds  10161  dvdsext  10167  sqrt2irr  10251  pw2dvdslemn  10253  pw2dvdseu  10256  qdencn  10511
  Copyright terms: Public domain W3C validator