= Replacement theorem for logical equivalence
Replacing a designated <subformula> by a logically equivalent <logical formula>[formula] preserves <logical equivalence> of the surrounding <propositional formulas>. For any <Boolean valuation> the two expressions at the replaced node have the same <truth value>. Each <logical connective> preserves this agreement when its other inputs are unchanged. Induction from that node to the root proves agreement of the whole <logical formula>[formulas] under every <Boolean valuation>[valuation].
Back to article page
