Theorem truan

True can be removed from a conjunction. (Contributed by FL, 20-Mar-2011.) (Proof shortened by Wolf Lammen, 21-Jul-2019.)

Conclusion

\( \vdash \top \wedge \varphi \leftrightarrow \varphi \)

Proof

tru

biantrur _

bicomi _