Theorem con3ALT
Proof of con3 from its associated inference con3i that illustrates the
use of the weak deduction theorem dedt. (Contributed by NM,
27-Jun-2002.) Revised to use the conditional operator. (Revised by BJ,
30-Sep-2019.) Revised dedt and elimh. (Revised by Steven Nguyen,
27-Apr-2023.) (Proof modification is discouraged.)
(New usage is discouraged.)
Conclusion
\( \vdash (\varphi \rightarrow \psi) \rightarrow \neg \psi \rightarrow \neg \varphi \)
Proof
id
notbid _
l2
imbi1d _
\( \vdash (\operatorname{if} ( \varphi \rightarrow \psi , \psi , \varphi ) \leftrightarrow \psi) \rightarrow (\neg \operatorname{if} ( \varphi \rightarrow \psi , \psi , \varphi ) \rightarrow \neg \varphi \leftrightarrow \neg \psi \rightarrow \neg \varphi) \)
l3
imbi2
\( \vdash (\operatorname{if} ( \varphi \rightarrow \psi , \psi , \varphi ) \leftrightarrow \psi) \rightarrow (\varphi \rightarrow \operatorname{if} ( \varphi \rightarrow \psi , \psi , \varphi ) \leftrightarrow \varphi \rightarrow \psi) \)
l4
imbi2
\( \vdash (\operatorname{if} ( \varphi \rightarrow \psi , \psi , \varphi ) \leftrightarrow \varphi) \rightarrow (\varphi \rightarrow \operatorname{if} ( \varphi \rightarrow \psi , \psi , \varphi ) \leftrightarrow \varphi \rightarrow \varphi) \)
id
\( \vdash \varphi \rightarrow \varphi \)
elimh l3 l4 _
con3i _
\( \vdash \neg \operatorname{if} ( \varphi \rightarrow \psi , \psi , \varphi ) \rightarrow \neg \varphi \)
dedt l2 _