Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  simprll 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  4981  fcof1  5423  mpt20  5574  eroveu  6197  addcmpblnq  6465  mulcmpblnq  6466  ordpipqqs  6472  addcmpblnq0  6541  mulcmpblnq0  6542  nnnq0lem1  6544  prarloclemcalc  6600  addlocpr  6634  distrlem4prl  6682  distrlem4pru  6683  ltpopr  6693  addcmpblnr  6824  mulcmpblnrlemg  6825  mulcmpblnr  6826  prsrlem1  6827  ltsrprg  6832  apreap  7578  apreim  7594  divdivdivap  7689  divmuleqap  7693  divadddivap  7703  divsubdivap  7704  ledivdiv  7856  lediv12a  7860  qbtwnz  9106  iseqcaopr  9242  leexp2r  9308  recvguniq  9593  rsqrmo  9625
 Copyright terms: Public domain W3C validator