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  6416  addcmpblnq0  6425  mulcmpblnq0  6426  nnnq0lem1  6428  prssnql  6461  prmuloc  6546  prmuloc2  6547  mullocpr  6551  ltexprlemopu  6576  ltexprlemrl  6583  ltexprlemru  6585  addcanprleml  6587  addcanprlemu  6588  ltmprr  6613  archpr  6614  addcmpblnr  6647  mulcmpblnrlemg  6648  mulcmpblnr  6649  ltsrprg  6655  negeu  6979  add20  7244  rimul  7349  apreap  7351  cru  7366  mulge0  7383  mulap0  7397  prodgt0  7579  ltmul12a  7587  ledivdiv  7617  lediv12a  7621  qapne  8330  qreccl  8331  ixxss12  8525  ioodisj  8611  fznlem  8655  elfz0fzfz0  8733  mulexpzap  8929  leexp1a  8943  expnbnd  9005  sqrtsq  9194
  Copyright terms: Public domain W3C validator