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

Theorem simpll 503
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 479 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ph )
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  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  simp1ll  1029  simp2ll  1033  simp3ll  1037  rmob  2973  prneimg  3671  exmid01  4091  pwntru  4092  ordtri2or2exmidlem  4411  onsucelsucexmidlem  4414  poinxp  4578  mpteqb  5479  fvmptt  5480  fcof1  5652  acexmid  5741  grprinvlem  5933  dftpos4  6128  tfrlem3ag  6174  tfrlem3a  6175  tfrlemi1  6197  tfrexlem  6199  tfr1onlem3ag  6202  nntr2  6367  dcdifsnid  6368  qsel  6474  ecopovsymg  6496  ecopoverg  6498  th3qlem1  6499  mapss  6553  xpmapenlem  6711  findcard2  6751  findcard2s  6752  findcard2sd  6754  unfiin  6782  f1finf1o  6803  fidcenumlemrk  6810  fidcenumlemr  6811  fidcenum  6812  sbthlemi6  6818  sbthlemi8  6820  elfi2  6828  supisolem  6863  enumct  6968  ismkvnex  6997  dfplpq2  7130  dfmpq2  7131  mulpipqqs  7149  distrnqg  7163  ltexnqq  7184  subhalfnqq  7190  prarloclemarch  7194  nnnq0lem1  7222  distrnq0  7235  npsspw  7247  prarloclemlo  7270  prarloclem3  7273  prarloclemcalc  7278  genplt2i  7286  distrlem1prl  7358  distrlem1pru  7359  distrlem4prl  7360  distrlem4pru  7361  ltprordil  7365  ltexprlemlol  7378  ltexprlemupu  7380  addextpr  7397  recexprlemopl  7401  recexprlemdisj  7406  recexprlem1ssl  7409  aptiprleml  7415  prsrlem1  7518  recexgt0sr  7549  addcnsr  7610  mulcnsr  7611  mulcnsrec  7619  axaddcl  7640  axmulcl  7642  axmulcom  7647  rereceu  7665  ltntri  7858  cnegexlem1  7905  cnegex  7908  addsub4  7973  le2add  8174  lt2add  8175  lt2sub  8190  le2sub  8191  rereim  8315  apreim  8332  mulreim  8333  addext  8339  mulext  8343  receuap  8397  rec11ap  8437  rec11rap  8438  divdivdivap  8440  ddcanap  8453  divadddivap  8454  divsubdivap  8455  conjmulap  8456  rerecclap  8457  recgt0  8572  prodgt0gt0  8573  prodgt0  8574  prodge0  8576  ltmul12a  8582  lemul12a  8584  lemulge11  8588  lt2mul2div  8601  ltrec  8605  lerec  8606  lt2msq  8608  ltrec1  8610  le2msq  8623  msq11  8624  ledivp1  8625  mulle0r  8666  peano5uzti  9117  eluzuzle  9290  qreccl  9390  xrltso  9537  z2ge  9564  xpncan  9609  xaddge0  9616  xle2add  9617  xleaddadd  9625  ixxss1  9642  ixxss2  9643  elioc2  9674  divelunit  9740  fzass4  9797  fzrev  9819  fzonmapblen  9919  elfzodifsumelfzo  9933  ssfzo12bi  9957  rebtwn2z  9987  qbtwnxr  9990  modqid  10077  modqcyc  10087  modqaddabs  10090  modqaddmod  10091  mulqaddmodid  10092  modqadd2mod  10102  modqltm1p1mod  10104  modqsubmod  10110  modqsubmodmod  10111  modqmulmod  10117  modqmulmodr  10118  modqsubdir  10121  frecuzrdgg  10144  seq3val  10186  seqvalcd  10187  seq3feq  10200  seq3f1olemp  10230  expp1  10255  expcl2lemap  10260  expnegzap  10282  expadd  10290  expmul  10293  leexp1a  10303  expnlbnd  10371  nn0opth2  10425  bcval  10450  bcval5  10464  bcpasc  10467  hashunsng  10508  seq3coll  10540  shftfvalg  10545  shftfval  10548  seq3shft  10565  caucvgrelemrec  10706  resqrexlemdecn  10739  sqrtmul  10762  sqrtdiv  10769  leabs  10801  absexpzap  10807  ltabs  10814  abslt  10815  absle  10816  abssubap0  10817  amgm2  10845  icodiamlt  10907  qdenre  10929  maxleim  10932  maxleastlt  10942  rexico  10948  zmaxcl  10951  minmax  10956  xrmaxleastlt  10980  xrminmax  10989  climuni  11017  cn1lem  11038  iserex  11063  iserle  11066  climserle  11069  climcau  11071  summodclem2a  11105  summodc  11107  isumss  11115  fisumss  11116  fsumadd  11130  isumadd  11155  fsum2dlemstep  11158  fsum2d  11159  fisum0diag2  11171  fsumabs  11189  isumsplit  11215  geolim  11235  geo2lim  11240  geoisum  11241  geoisumr  11242  geoisum1  11243  mertenslemub  11258  mertenslemi1  11259  mertenslem2  11260  mertensabs  11261  efcvgfsum  11287  eftlcl  11308  reeftlcl  11309  tanaddap  11360  zdvdsdc  11426  dvds2ln  11438  dvdsle  11454  divconjdvds  11459  dvdsext  11465  gcdsupex  11558  gcdsupcl  11559  bezoutlemmain  11598  bezoutlemaz  11603  bezoutlembi  11605  bezout  11611  gcdmultiplez  11621  dvdsmulgcd  11625  bezoutr  11632  bezoutr1  11633  lcmval  11656  lcmcllem  11660  ncoprmgcdne1b  11682  cncongr1  11696  prmdvdsexp  11738  sqrt2irr  11752  pw2dvdslemn  11754  pw2dvdseu  11757  nonsq  11796  isstruct2r  11881  setsfun  11905  setsfun0  11906  neissex  12245  tgrest  12249  ssrest  12262  restopn2  12263  cnco  12301  cnss1  12306  cnss2  12307  cnptopresti  12318  uptx  12354  txrest  12356  psmetres2  12413  xmetres2  12459  xblss2ps  12484  blhalf  12488  blssexps  12509  blssex  12510  blin2  12512  blbas  12513  bdmetval  12580  metcnpi  12595  metcnpi2  12596  qtopbas  12602  tgqioo  12627  cncfss  12650  mulc1cncf  12656  cncfmptid  12663  dedekindicc  12691  ivthdec  12702  cnplimcim  12716  cnplimclemle  12717  cnplimccntop  12719  limccnp2cntop  12726  dvfgg  12737  dvcj  12753  dvrecap  12757  dveflem  12766  ptolemy  12816  pwtrufal  13088  nninfalllem1  13099  nninfsellemqall  13107  sbthom  13117  qdencn  13118  isomninnlem  13121
  Copyright terms: Public domain W3C validator