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

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

Proof of Theorem simprll
StepHypRef Expression
1 simpl 102 . 2 ((ψ χ) → ψ)
21ad2antrl 459 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:  imain  4924  fcof1  5366  mpt20  5516  eroveu  6133  addcmpblnq  6351  mulcmpblnq  6352  ordpipqqs  6358  addcmpblnq0  6426  mulcmpblnq0  6427  nnnq0lem1  6429  prarloclemcalc  6485  addlocpr  6519  distrlem4prl  6560  distrlem4pru  6561  ltpopr  6569  addcmpblnr  6667  mulcmpblnrlemg  6668  mulcmpblnr  6669  prsrlem1  6670  ltsrprg  6675  apreap  7371  apreim  7387  divdivdivap  7471  divmuleqap  7475  divadddivap  7485  divsubdivap  7486  ledivdiv  7637  lediv12a  7641  leexp2r  8962
  Copyright terms: Public domain W3C validator