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

Theorem simpllr 486
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
Assertion
Ref Expression
simpllr ((((φ ψ) χ) θ) → ψ)

Proof of Theorem simpllr
StepHypRef Expression
1 simpr 103 . 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:  f1o2ndf1  5791  tfrlem1  5864  fopwdom  6246  addcmpblnq  6351  mulcmpblnq  6352  ordpipqqs  6358  ltexnqq  6391  enq0tr  6417  addcmpblnq0  6426  mulcmpblnq0  6427  nnnq0lem1  6429  prssnqu  6463  prarloclemup  6478  nqprl  6533  mullocpr  6552  cauappcvgprlemladdfu  6626  cauappcvgprlemladdrl  6629  caucvgprlemm  6639  caucvgprlemladdfu  6648  caucvgprlemladdrl  6649  caucvgprlemlim  6652  addcmpblnr  6667  mulcmpblnrlemg  6668  mulcmpblnr  6669  ltsrprg  6675  cnegexlem3  6985  negeu  6999  add20  7264  rimul  7369  apreap  7371  cru  7386  apreim  7387  apsym  7390  apcotr  7391  apadd1  7392  apneg  7395  mulext1  7396  apti  7406  mulap0  7417  prodgt0  7599  ltmul12a  7607  ledivdiv  7637  lediv12a  7641  qapne  8350  ixxss12  8545  ioodisj  8631  fznlem  8675  mulexpzap  8949  leexp1a  8963  expnbnd  9025  cjap  9134  sqrtsq  9214
  Copyright terms: Public domain W3C validator