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

Theorem simpll 501
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 477 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  1027  simp2ll  1031  simp3ll  1035  rmob  2971  prneimg  3669  exmid01  4089  pwntru  4090  ordtri2or2exmidlem  4409  onsucelsucexmidlem  4412  poinxp  4576  mpteqb  5477  fvmptt  5478  fcof1  5650  acexmid  5739  grprinvlem  5931  dftpos4  6126  tfrlem3ag  6172  tfrlem3a  6173  tfrlemi1  6195  tfrexlem  6197  tfr1onlem3ag  6200  nntr2  6365  dcdifsnid  6366  qsel  6472  ecopovsymg  6494  ecopoverg  6496  th3qlem1  6497  mapss  6551  xpmapenlem  6709  findcard2  6749  findcard2s  6750  findcard2sd  6752  unfiin  6780  f1finf1o  6801  fidcenumlemrk  6808  fidcenumlemr  6809  fidcenum  6810  sbthlemi6  6816  sbthlemi8  6818  elfi2  6826  supisolem  6861  enumct  6966  ismkvnex  6995  dfplpq2  7126  dfmpq2  7127  mulpipqqs  7145  distrnqg  7159  ltexnqq  7180  subhalfnqq  7186  prarloclemarch  7190  nnnq0lem1  7218  distrnq0  7231  npsspw  7243  prarloclemlo  7266  prarloclem3  7269  prarloclemcalc  7274  genplt2i  7282  distrlem1prl  7354  distrlem1pru  7355  distrlem4prl  7356  distrlem4pru  7357  ltprordil  7361  ltexprlemlol  7374  ltexprlemupu  7376  addextpr  7393  recexprlemopl  7397  recexprlemdisj  7402  recexprlem1ssl  7405  aptiprleml  7411  prsrlem1  7514  recexgt0sr  7545  addcnsr  7606  mulcnsr  7607  mulcnsrec  7615  axaddcl  7636  axmulcl  7638  axmulcom  7643  rereceu  7661  ltntri  7854  cnegexlem1  7901  cnegex  7904  addsub4  7969  le2add  8170  lt2add  8171  lt2sub  8186  le2sub  8187  rereim  8311  apreim  8328  mulreim  8329  addext  8335  mulext  8339  receuap  8393  rec11ap  8433  rec11rap  8434  divdivdivap  8436  ddcanap  8449  divadddivap  8450  divsubdivap  8451  conjmulap  8452  rerecclap  8453  recgt0  8568  prodgt0gt0  8569  prodgt0  8570  prodge0  8572  ltmul12a  8578  lemul12a  8580  lemulge11  8584  lt2mul2div  8597  ltrec  8601  lerec  8602  lt2msq  8604  ltrec1  8606  le2msq  8619  msq11  8620  ledivp1  8621  mulle0r  8662  peano5uzti  9113  eluzuzle  9286  qreccl  9386  xrltso  9533  z2ge  9560  xpncan  9605  xaddge0  9612  xle2add  9613  xleaddadd  9621  ixxss1  9638  ixxss2  9639  elioc2  9670  divelunit  9736  fzass4  9793  fzrev  9815  fzonmapblen  9915  elfzodifsumelfzo  9929  ssfzo12bi  9953  rebtwn2z  9983  qbtwnxr  9986  modqid  10073  modqcyc  10083  modqaddabs  10086  modqaddmod  10087  mulqaddmodid  10088  modqadd2mod  10098  modqltm1p1mod  10100  modqsubmod  10106  modqsubmodmod  10107  modqmulmod  10113  modqmulmodr  10114  modqsubdir  10117  frecuzrdgg  10140  seq3val  10182  seqvalcd  10183  seq3feq  10196  seq3f1olemp  10226  expp1  10251  expcl2lemap  10256  expnegzap  10278  expadd  10286  expmul  10289  leexp1a  10299  expnlbnd  10367  nn0opth2  10421  bcval  10446  bcval5  10460  bcpasc  10463  hashunsng  10504  seq3coll  10536  shftfvalg  10541  shftfval  10544  seq3shft  10561  caucvgrelemrec  10702  resqrexlemdecn  10735  sqrtmul  10758  sqrtdiv  10765  leabs  10797  absexpzap  10803  ltabs  10810  abslt  10811  absle  10812  abssubap0  10813  amgm2  10841  icodiamlt  10903  qdenre  10925  maxleim  10928  maxleastlt  10938  rexico  10944  zmaxcl  10947  minmax  10952  xrmaxleastlt  10976  xrminmax  10985  climuni  11013  cn1lem  11034  iserex  11059  iserle  11062  climserle  11065  climcau  11067  summodclem2a  11101  summodc  11103  isumss  11111  fisumss  11112  fsumadd  11126  isumadd  11151  fsum2dlemstep  11154  fsum2d  11155  fisum0diag2  11167  fsumabs  11185  isumsplit  11211  geolim  11231  geo2lim  11236  geoisum  11237  geoisumr  11238  geoisum1  11239  mertenslemub  11254  mertenslemi1  11255  mertenslem2  11256  mertensabs  11257  efcvgfsum  11283  eftlcl  11304  reeftlcl  11305  tanaddap  11356  zdvdsdc  11421  dvds2ln  11433  dvdsle  11449  divconjdvds  11454  dvdsext  11460  gcdsupex  11553  gcdsupcl  11554  bezoutlemmain  11593  bezoutlemaz  11598  bezoutlembi  11600  bezout  11606  gcdmultiplez  11616  dvdsmulgcd  11620  bezoutr  11627  bezoutr1  11628  lcmval  11651  lcmcllem  11655  ncoprmgcdne1b  11677  cncongr1  11691  prmdvdsexp  11733  sqrt2irr  11747  pw2dvdslemn  11749  pw2dvdseu  11752  nonsq  11791  isstruct2r  11876  setsfun  11900  setsfun0  11901  neissex  12240  tgrest  12244  ssrest  12257  restopn2  12258  cnco  12296  cnss1  12301  cnss2  12302  cnptopresti  12313  uptx  12349  txrest  12351  psmetres2  12408  xmetres2  12454  xblss2ps  12479  blhalf  12483  blssexps  12504  blssex  12505  blin2  12507  blbas  12508  bdmetval  12575  metcnpi  12590  metcnpi2  12591  qtopbas  12597  tgqioo  12622  cncfss  12645  mulc1cncf  12651  cncfmptid  12658  dedekindicc  12686  ivthdec  12697  cnplimcim  12711  cnplimclemle  12712  cnplimccntop  12714  limccnp2cntop  12721  dvfgg  12732  dvcj  12748  dvrecap  12752  dveflem  12761  pwtrufal  13026  nninfalllem1  13037  nninfsellemqall  13045  sbthom  13055  qdencn  13056  isomninnlem  13059
  Copyright terms: Public domain W3C validator