Theorem dedt

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
dedt.1
\( \vdash (\operatorname{if} ( \chi , \varphi , \psi ) \leftrightarrow \varphi) \rightarrow (\tau \leftrightarrow \theta) \)
dedt.2
\( \vdash \tau \)
Conclusion
\( \vdash \chi \rightarrow \theta \)
Proof
l0
ifptru
\( \vdash \chi \rightarrow (\operatorname{if} ( \chi , \varphi , \psi ) \leftrightarrow \varphi) \)
l1
dedt.2
\( \vdash \tau \)
dedt.1
\( \vdash (\operatorname{if} ( \chi , \varphi , \psi ) \leftrightarrow \varphi) \rightarrow (\tau \leftrightarrow \theta) \)
mpbii l1 _
\( \vdash (\operatorname{if} ( \chi , \varphi , \psi ) \leftrightarrow \varphi) \rightarrow \theta \)
syl l0 _