Theorem
3anim2i
Add two conjuncts to antecedent and consequent. (Contributed by AV, 21-Nov-2019.)
Hypothesis
3animi.1
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \chi \wedge \varphi \wedge \theta \rightarrow \chi \wedge \psi \wedge \theta \)
Proof
l0
id
l1
3animi.1
id
3anim123i
l0
l1
_
This is the content in the right pane.