ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  simpll Structured version   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  6428  distrnq0  6441  npsspw  6453  prarloclemlo  6476  prarloclem3  6479  prarloclemcalc  6484  genplt2i  6492  distrlem1prl  6557  distrlem1pru  6558  distrlem4prl  6559  distrlem4pru  6560  ltprordil  6564  ltexprlemlol  6575  ltexprlemupu  6577  addextpr  6592  recexprlemopl  6596  recexprlemdisj  6601  recexprlem1ssl  6604  aptiprleml  6610  prsrlem1  6650  recexgt0sr  6681  addcnsr  6711  mulcnsr  6712  mulcnsrec  6720  axaddcl  6730  axmulcl  6732  axmulcom  6735  cnegexlem1  6963  cnegex  6966  addsub4  7030  le2add  7214  lt2add  7215  lt2sub  7230  le2sub  7231  rereim  7350  apreim  7367  mulreim  7368  addext  7374  mulext  7378  receuap  7412  rec11ap  7448  rec11rap  7449  divdivdivap  7451  ddcanap  7464  divadddivap  7465  divsubdivap  7466  conjmulap  7467  rerecclap  7468  recgt0  7577  prodgt0gt0  7578  prodgt0  7579  prodge0  7581  ltmul12a  7587  lemul12a  7589  lemulge11  7593  lt2mul2div  7606  ltrec  7610  lerec  7611  lt2msq  7613  ltrec1  7615  le2msq  7628  msq11  7629  ledivp1  7630  peano5uzti  8102  eluzuzle  8237  qreccl  8331  xrltso  8467  z2ge  8489  ixxss1  8523  ixxss2  8524  elioc2  8555  divelunit  8620  fzass4  8675  fzrev  8696  fzonmapblen  8793  elfzodifsumelfzo  8807  ssfzo12bi  8831  expivallem  8890  expp1  8896  expcl2lemap  8901  expnegzap  8923  expadd  8931  expmul  8934  leexp1a  8943  expnlbnd  9006
  Copyright terms: Public domain W3C validator