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

Theorem simpll 481
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 457 1 (((φ ψ) χ) → φ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem is referenced by:  simp1ll  966  simp2ll  970  simp3ll  974  rmob  2844  prneimg  3536  onsucelsucexmidlem  4214  poinxp  4352  mpteqb  5204  fvmptt  5205  fcof1  5366  acexmid  5454  grprinvlem  5637  dftpos4  5819  tfrlem3ag  5865  tfrlem3a  5866  tfrlemi1  5887  tfrexlem  5889  qsel  6119  ecopovsymg  6141  ecopoverg  6143  th3qlem1  6144  dfplpq2  6338  dfmpq2  6339  mulpipqqs  6357  distrnqg  6371  ltexnqq  6391  subhalfnqq  6397  prarloclemarch  6401  nnnq0lem1  6429  distrnq0  6442  npsspw  6454  prarloclemlo  6477  prarloclem3  6480  prarloclemcalc  6485  genplt2i  6493  distrlem1prl  6558  distrlem1pru  6559  distrlem4prl  6560  distrlem4pru  6561  ltprordil  6565  ltexprlemlol  6576  ltexprlemupu  6578  addextpr  6593  recexprlemopl  6597  recexprlemdisj  6602  recexprlem1ssl  6605  aptiprleml  6611  prsrlem1  6670  recexgt0sr  6701  addcnsr  6731  mulcnsr  6732  mulcnsrec  6740  axaddcl  6750  axmulcl  6752  axmulcom  6755  cnegexlem1  6983  cnegex  6986  addsub4  7050  le2add  7234  lt2add  7235  lt2sub  7250  le2sub  7251  rereim  7370  apreim  7387  mulreim  7388  addext  7394  mulext  7398  receuap  7432  rec11ap  7468  rec11rap  7469  divdivdivap  7471  ddcanap  7484  divadddivap  7485  divsubdivap  7486  conjmulap  7487  rerecclap  7488  recgt0  7597  prodgt0gt0  7598  prodgt0  7599  prodge0  7601  ltmul12a  7607  lemul12a  7609  lemulge11  7613  lt2mul2div  7626  ltrec  7630  lerec  7631  lt2msq  7633  ltrec1  7635  le2msq  7648  msq11  7649  ledivp1  7650  peano5uzti  8122  eluzuzle  8257  qreccl  8351  xrltso  8487  z2ge  8509  ixxss1  8543  ixxss2  8544  elioc2  8575  divelunit  8640  fzass4  8695  fzrev  8716  fzonmapblen  8813  elfzodifsumelfzo  8827  ssfzo12bi  8851  expivallem  8910  expp1  8916  expcl2lemap  8921  expnegzap  8943  expadd  8951  expmul  8954  leexp1a  8963  expnlbnd  9026
  Copyright terms: Public domain W3C validator