Theorem biort

A disjunction with a true formula is equivalent to that true formula. (Contributed by NM, 23-May-1999.)

Conclusion
\( \vdash \varphi \rightarrow (\varphi \leftrightarrow \varphi \vee \psi) \)
Proof
l0
id
orc
2thd l0 _