<?xml version="1.0"?>
<div>:: <span class="kw">deftheorem </span>   defines <a href="intpro_2.html#V1" title="INTPRO_2:attr.1">valid_IPC</a> <a onclick="hs(this)" href="javascript:()">INTPRO_2:def 9 : <br/></a><span> for <font color="Olive" title="b1">s</font> being   <a href="intpro_1.html#NM1" title="INTPRO_1:NM.1">MC-formula</a> holds <br/> ( <font color="Olive" title="b1">s</font> is  <a href="intpro_2.html#V1" title="INTPRO_2:attr.1">valid_IPC</a>  iff <font color="Olive" title="b1">s</font> <a href="tarski.html#R2" title="TARSKI:pred.2">in</a>  <a href="intpro_1.html#K8" title="INTPRO_1:func.8">IPC-Taut</a>  );<br/></span></div>
