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

Theorem simpll 469
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 460 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  953  simp2ll  957  simp3ll  961  rmob  2823  prneimg  3515  onsucelsucexmidlem  4194  poinxp  4332  mpteqb  5182  fvmptt  5183  fcof1  5344  acexmid  5431  grprinvlem  5614  dftpos4  5796  tfrlem3ag  5842  tfrlem3a  5843  tfrlemi1  5863  tfrexlem  5866  qsel  6090  ecopovsymg  6112  ecopoverg  6114  th3qlem1  6115  dfplpq2  6207  dfmpq2  6208  mulpipqqs  6226  distrnqg  6240  ltexnqq  6260  subhalfnqq  6265  prarloclemarch  6269  nnnq0lem1  6295  distrnq0  6308  npsspw  6319  prarloclemlo  6342  prarloclem3  6345  prarloclemcalc  6350  genplt2i  6358  distrlem1prl  6415  distrlem1pru  6416  distrlem4prl  6417  distrlem4pru  6418  ltprordil  6422  ltexprlemlol  6433  ltexprlemupu  6435  recexprlemopl  6453  recexprlemdisj  6458  recexprlem1ssl  6461  prsrlem1  6483  recexsrlem  6514  addcnsr  6539  mulcnsr  6540  mulcnsrec  6548  axaddcl  6554  axmulcl  6556  axmulcom  6559  cnegexlem1  6773  cnegex  6776  addsub4  6840  le2add  7024  lt2add  7025  lt2sub  7040  le2sub  7041
  Copyright terms: Public domain W3C validator