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

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

Proof of Theorem simplll
StepHypRef Expression
1 simpl 102 . 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:  f1imass  5356  tfrlem1  5864  addcmpblnq  6351  mulcmpblnq  6352  ordpipqqs  6358  ltexnqq  6391  enq0tr  6417  addcmpblnq0  6426  mulcmpblnq0  6427  nnnq0lem1  6429  prssnql  6462  prmuloc  6547  prmuloc2  6548  mullocpr  6552  ltexprlemopu  6577  ltexprlemrl  6584  ltexprlemru  6586  addcanprleml  6588  addcanprlemu  6589  ltmprr  6614  archpr  6615  addcmpblnr  6667  mulcmpblnrlemg  6668  mulcmpblnr  6669  ltsrprg  6675  negeu  6999  add20  7264  rimul  7369  apreap  7371  cru  7386  mulge0  7403  mulap0  7417  prodgt0  7599  ltmul12a  7607  ledivdiv  7637  lediv12a  7641  qapne  8350  qreccl  8351  ixxss12  8545  ioodisj  8631  fznlem  8675  elfz0fzfz0  8753  mulexpzap  8949  leexp1a  8963  expnbnd  9025  sqrtsq  9214
  Copyright terms: Public domain W3C validator