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

Theorem simprll 504
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
Assertion
Ref Expression
simprll ((𝜑 ∧ ((𝜓𝜒) ∧ 𝜃)) → 𝜓)

Proof of Theorem simprll
StepHypRef Expression
1 simpl 107 . 2 ((𝜓𝜒) → 𝜓)
21ad2antrl 474 1 ((𝜑 ∧ ((𝜓𝜒) ∧ 𝜃)) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  imain  5012  fcof1  5454  mpt20  5605  eroveu  6263  addcmpblnq  6619  mulcmpblnq  6620  ordpipqqs  6626  addcmpblnq0  6695  mulcmpblnq0  6696  nnnq0lem1  6698  prarloclemcalc  6754  addlocpr  6788  distrlem4prl  6836  distrlem4pru  6837  ltpopr  6847  addcmpblnr  6978  mulcmpblnrlemg  6979  mulcmpblnr  6980  prsrlem1  6981  ltsrprg  6986  apreap  7754  apreim  7770  divdivdivap  7868  divmuleqap  7872  divadddivap  7882  divsubdivap  7883  ledivdiv  8035  lediv12a  8039  exbtwnz  9337  iseqcaopr  9558  leexp2r  9627  recvguniq  10019  rsqrmo  10051  qredeu  10623  pw2dvdseu  10690
  Copyright terms: Public domain W3C validator