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

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

Proof of Theorem simprlr
StepHypRef Expression
1 simpr 108 . 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  5032  fcof1  5475  fliftfun  5488  addcmpblnq  6689  mulcmpblnq  6690  ordpipqqs  6696  enq0tr  6756  addcmpblnq0  6765  mulcmpblnq0  6766  nnnq0lem1  6768  addnq0mo  6769  mulnq0mo  6770  prarloclemcalc  6824  addlocpr  6858  distrlem4prl  6906  distrlem4pru  6907  addcmpblnr  7048  mulcmpblnrlemg  7049  mulcmpblnr  7050  prsrlem1  7051  addsrmo  7052  mulsrmo  7053  ltsrprg  7056  apreap  7824  apreim  7840  divdivdivap  7938  divsubdivap  7953  ledivdiv  8105  lediv12a  8109  exbtwnz  9407  iseqcaopr  9628  leexp2r  9697  recvguniq  10100  rsqrmo  10132  qredeu  10704  pw2dvdseu  10771
  Copyright terms: Public domain W3C validator