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

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

Proof of Theorem simprll
StepHypRef Expression
1 simpl 108 . 2 ((𝜓𝜒) → 𝜓)
21ad2antrl 475 1 ((𝜑 ∧ ((𝜓𝜒) ∧ 𝜃)) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  imain  5130  fcof1  5600  mpt20  5756  eroveu  6423  sbthlemi6  6751  sbthlemi8  6753  addcmpblnq  7023  mulcmpblnq  7024  ordpipqqs  7030  addcmpblnq0  7099  mulcmpblnq0  7100  nnnq0lem1  7102  prarloclemcalc  7158  addlocpr  7192  distrlem4prl  7240  distrlem4pru  7241  ltpopr  7251  addcmpblnr  7382  mulcmpblnrlemg  7383  mulcmpblnr  7384  prsrlem1  7385  ltsrprg  7390  apreap  8161  apreim  8177  divdivdivap  8277  divmuleqap  8281  divadddivap  8291  divsubdivap  8292  ledivdiv  8448  lediv12a  8452  exbtwnz  9811  seq3caopr  10033  leexp2r  10124  zfz1iso  10361  recvguniq  10543  rsqrmo  10575  summodclem2  10925  qredeu  11506  pw2dvdseu  11573  epttop  11942  metequiv2  12282  mulc1cncf  12344  cncfmptc  12348  cncfmptid  12349  addccncf  12351  negcncf  12353
  Copyright terms: Public domain W3C validator