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

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

Proof of Theorem simprlr
StepHypRef Expression
1 simpr 103 . 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  fliftfun  5436  addcmpblnq  6463  mulcmpblnq  6464  ordpipqqs  6470  enq0tr  6530  addcmpblnq0  6539  mulcmpblnq0  6540  nnnq0lem1  6542  addnq0mo  6543  mulnq0mo  6544  prarloclemcalc  6598  addlocpr  6632  distrlem4prl  6680  distrlem4pru  6681  addcmpblnr  6822  mulcmpblnrlemg  6823  mulcmpblnr  6824  prsrlem1  6825  addsrmo  6826  mulsrmo  6827  ltsrprg  6830  apreap  7576  apreim  7592  divdivdivap  7687  divsubdivap  7702  ledivdiv  7854  lediv12a  7858  qbtwnz  9104  iseqcaopr  9216  leexp2r  9282  recvguniq  9567  rsqrmo  9599
  Copyright terms: Public domain W3C validator