Theorem elimh
Hypothesis builder for the weak deduction theorem. For more
information, see the Weak Deduction Theorem page [mmdeduction.html].
(Contributed by NM, 26-Jun-2002.) Revised to use the conditional
operator. (Revised by BJ, 30-Sep-2019.) Commute consequent. (Revised
by Steven Nguyen, 27-Apr-2023.)
Hypotheses
elimh.1
\( \vdash (\operatorname{if} ( \chi , \varphi , \psi ) \leftrightarrow \varphi) \rightarrow (\tau \leftrightarrow \chi) \)
elimh.2
\( \vdash (\operatorname{if} ( \chi , \varphi , \psi ) \leftrightarrow \psi) \rightarrow (\tau \leftrightarrow \theta) \)
elimh.3
\( \vdash \theta \)
Conclusion
\( \vdash \tau \)
Proof
l0
ifptru
\( \vdash \chi \rightarrow (\operatorname{if} ( \chi , \varphi , \psi ) \leftrightarrow \varphi) \)
elimh.1
\( \vdash (\operatorname{if} ( \chi , \varphi , \psi ) \leftrightarrow \varphi) \rightarrow (\tau \leftrightarrow \chi) \)
syl l0 _
l3
ibir _
\( \vdash \chi \rightarrow \tau \)
l4
elimh.3
\( \vdash \theta \)
l5
ifpfal
\( \vdash \neg \chi \rightarrow (\operatorname{if} ( \chi , \varphi , \psi ) \leftrightarrow \psi) \)
elimh.2
\( \vdash (\operatorname{if} ( \chi , \varphi , \psi ) \leftrightarrow \psi) \rightarrow (\tau \leftrightarrow \theta) \)
syl l5 _
\( \vdash \neg \chi \rightarrow (\tau \leftrightarrow \theta) \)
mpbiri l4 _
\( \vdash \neg \chi \rightarrow \tau \)
pm2.61i l3 _