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

Theorem simplr 470
Description: Simplification of a conjunction. (Contributed by NM, 20-Mar-2007.)
Assertion
Ref Expression
simplr (((φ ψ) χ) → ψ)

Proof of Theorem simplr
StepHypRef Expression
1 id 19 . 2 (ψψ)
21ad2antlr 462 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:  simp1lr  954  simp2lr  958  simp3lr  962  bilukdc  1268  intab  3614  imadiflem  4900  fvmptt  5183  fcoconst  5255  f1imass  5334  fcof1  5344  fliftfun  5357  riotass2  5414  ovmpt2dxf  5545  dftpos4  5796  tfrlem1  5841  tfrlem3ag  5842  tfrlemibacc  5857  tfrlemibfn  5859  tfrlemi1  5863  tfrlemi14d  5864  nnm00  6009  ecopovsymg  6112  ecopoverg  6114  th3qlem1  6115  dfplpq2  6207  dfmpq2  6208  mulpipqqs  6226  nqpi  6231  distrnqg  6240  prarloclemarch  6269  enq0tr  6283  nqnq0pi  6287  nq0nn  6291  nnnq0lem1  6295  prarloclemup  6343  prarloclem3  6345  prarloclemcalc  6350  genplt2i  6358  addnqprllem  6376  addnqprulem  6377  appdivnq  6401  distrlem1prl  6415  distrlem1pru  6416  ltaddpr  6428  ltexprlemlol  6433  ltexprlemupu  6435  ltexprlemdisj  6437  addcanprleml  6445  ltaprlem  6448  recexprlemopu  6455  recexprlemdisj  6458  recexprlem1ssl  6461  aptiprleml  6467  prsrlem1  6486  recexgt0sr  6517  mulgt0sr  6520  addcnsr  6544  mulcnsr  6545  mulcnsrec  6553  axmulcom  6564  cnegexlem2  6789  cnegexlem3  6790  addsub4  6855  le2add  7039  lt2add  7040  lt2sub  7055  le2sub  7056  rereim  7175  apreim  7188  apcotr  7191  apadd1  7192  extadd  7194
  Copyright terms: Public domain W3C validator