Theorem had1OLD
Obsolete version of had1 as of 10-Aug-2026. (Contributed by Mario
Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 11-Jul-2020.)
(Proof modification is discouraged.) (New usage is discouraged.)
Conclusion
\( \vdash \varphi \rightarrow (\text{ hadd } ( \varphi , \psi , \chi ) \leftrightarrow (\psi \leftrightarrow \chi)) \)
Proof
l0
hadrot
\( \vdash \text{ hadd } ( \varphi , \psi , \chi ) \leftrightarrow \text{ hadd } ( \psi , \chi , \varphi ) \)
hadbi
\( \vdash \text{ hadd } ( \psi , \chi , \varphi ) \leftrightarrow (\psi \leftrightarrow \chi \leftrightarrow \varphi) \)
l2
bitri l0 _
\( \vdash \text{ hadd } ( \varphi , \psi , \chi ) \leftrightarrow (\psi \leftrightarrow \chi \leftrightarrow \varphi) \)
biass
\( \vdash \text{ hadd } ( \varphi , \psi , \chi ) \leftrightarrow (\psi \leftrightarrow \chi) \leftrightarrow \varphi \leftrightarrow (\text{ hadd } ( \varphi , \psi , \chi ) \leftrightarrow (\psi \leftrightarrow \chi \leftrightarrow \varphi)) \)
mpbir l2 _
biimpri _