We describe a general method how to construct from a propositional proof system P a possibly much stronger proof system iP. The system iP operates with exponentially long P-proofs described ``implicitly'' by polynomial size circuits. As an example we prove that proof system iEF, implicit EF, corresponds to bounded arithmetic ... more >>>