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

Theorem simpll 503
Description: Simplification of a conjunction. (Contributed by NM, 18-Mar-2007.)
Assertion
Ref Expression
simpll (((𝜑𝜓) ∧ 𝜒) → 𝜑)

Proof of Theorem simpll
StepHypRef Expression
1 id 19 . 2 (𝜑𝜑)
21ad2antrr 479 1 (((𝜑𝜓) ∧ 𝜒) → 𝜑)
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  8316  apreim  8333  mulreim  8334  addext  8340  mulext  8344  receuap  8398  rec11ap  8438  rec11rap  8439  divdivdivap  8441  ddcanap  8454  divadddivap  8455  divsubdivap  8456  conjmulap  8457  rerecclap  8458  subrecap  8566  recgt0  8576  prodgt0gt0  8577  prodgt0  8578  prodge0  8580  ltmul12a  8586  lemul12a  8588  lemulge11  8592  lt2mul2div  8605  ltrec  8609  lerec  8610  lt2msq  8612  ltrec1  8614  le2msq  8627  msq11  8628  ledivp1  8629  mulle0r  8670  peano5uzti  9127  eluzuzle  9302  qreccl  9402  xrltso  9550  z2ge  9577  xpncan  9622  xaddge0  9629  xle2add  9630  xleaddadd  9638  ixxss1  9655  ixxss2  9656  elioc2  9687  divelunit  9753  fzass4  9810  fzrev  9832  fzonmapblen  9932  elfzodifsumelfzo  9946  ssfzo12bi  9970  rebtwn2z  10000  qbtwnxr  10003  modqid  10090  modqcyc  10100  modqaddabs  10103  modqaddmod  10104  mulqaddmodid  10105  modqadd2mod  10115  modqltm1p1mod  10117  modqsubmod  10123  modqsubmodmod  10124  modqmulmod  10130  modqmulmodr  10131  modqsubdir  10134  frecuzrdgg  10157  seq3val  10199  seqvalcd  10200  seq3feq  10213  seq3f1olemp  10243  expp1  10268  expcl2lemap  10273  expnegzap  10295  expadd  10303  expmul  10306  leexp1a  10316  expnlbnd  10384  nn0opth2  10438  bcval  10463  bcval5  10477  bcpasc  10480  hashunsng  10521  seq3coll  10553  shftfvalg  10558  shftfval  10561  seq3shft  10578  caucvgrelemrec  10719  resqrexlemdecn  10752  sqrtmul  10775  sqrtdiv  10782  leabs  10814  absexpzap  10820  ltabs  10827  abslt  10828  absle  10829  abssubap0  10830  amgm2  10858  icodiamlt  10920  qdenre  10942  maxleim  10945  maxleastlt  10955  rexico  10961  zmaxcl  10964  minmax  10969  xrmaxleastlt  10993  xrminmax  11002  climuni  11030  cn1lem  11051  iserex  11076  iserle  11079  climserle  11082  climcau  11084  summodclem2a  11118  summodc  11120  isumss  11128  fisumss  11129  fsumadd  11143  isumadd  11168  fsum2dlemstep  11171  fsum2d  11172  fisum0diag2  11184  fsumabs  11202  isumsplit  11228  geolim  11248  geo2lim  11253  geoisum  11254  geoisumr  11255  geoisum1  11256  mertenslemub  11271  mertenslemi1  11272  mertenslem2  11273  mertensabs  11274  efcvgfsum  11300  eftlcl  11321  reeftlcl  11322  tanaddap  11373  zdvdsdc  11441  dvds2ln  11453  dvdsle  11469  divconjdvds  11474  dvdsext  11480  gcdsupex  11573  gcdsupcl  11574  bezoutlemmain  11613  bezoutlemaz  11618  bezoutlembi  11620  bezout  11626  gcdmultiplez  11636  dvdsmulgcd  11640  bezoutr  11647  bezoutr1  11648  lcmval  11671  lcmcllem  11675  ncoprmgcdne1b  11697  cncongr1  11711  prmdvdsexp  11753  sqrt2irr  11767  pw2dvdslemn  11770  pw2dvdseu  11773  nonsq  11812  isstruct2r  11897  setsfun  11921  setsfun0  11922  neissex  12261  tgrest  12265  ssrest  12278  restopn2  12279  cnco  12317  cnss1  12322  cnss2  12323  cnptopresti  12334  uptx  12370  txrest  12372  psmetres2  12429  xmetres2  12475  xblss2ps  12500  blhalf  12504  blssexps  12525  blssex  12526  blin2  12528  blbas  12529  bdmetval  12596  metcnpi  12611  metcnpi2  12612  qtopbas  12618  tgqioo  12643  cncfss  12666  mulc1cncf  12672  cncfmptid  12679  dedekindicc  12707  ivthdec  12718  cnplimcim  12732  cnplimclemle  12733  cnplimccntop  12735  limccnp2cntop  12742  dvfgg  12753  dvcj  12769  dvrecap  12773  dveflem  12782  ptolemy  12832  pwtrufal  13119  nninfalllem1  13130  nninfsellemqall  13138  sbthom  13148  qdencn  13149  isomninnlem  13152
  Copyright terms: Public domain W3C validator