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  6425  mulcmpblnq0  6426  nnnq0lem1  6428  prarloclemcalc  6484  addlocpr  6518  distrlem4prl  6559  distrlem4pru  6560  ltpopr  6568  addcmpblnr  6647  mulcmpblnrlemg  6648  mulcmpblnr  6649  prsrlem1  6650  ltsrprg  6655  apreap  7351  apreim  7367  divdivdivap  7451  divmuleqap  7455  divadddivap  7465  divsubdivap  7466  ledivdiv  7617  lediv12a  7621  leexp2r  8942
  Copyright terms: Public domain W3C validator