Theorem tsim1

Description: A Tseitin axiom for logical implication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018)

	Ref	Expression
Assertion	tsim1	$$⊢\theta \to \left(\left(\neg \phi \vee \psi \right)\vee \neg \left(\phi \to \psi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		exmid	$$⊢\left(\left(\phi \to \psi \right)\vee \neg \left(\phi \to \psi \right)\right)$$
2		df-or	$$⊢\left(\neg \phi \vee \psi \right)\leftrightarrow \left(\neg \neg \phi \to \psi \right)$$
3		notnotb	$$⊢\phi \leftrightarrow \neg \neg \phi$$
4	3	bicomi	$$⊢\neg \neg \phi \leftrightarrow \phi$$
5	4	imbi1i	$$⊢\left(\neg \neg \phi \to \psi \right)\leftrightarrow \left(\phi \to \psi \right)$$
6	2 5	bitri	$$⊢\left(\neg \phi \vee \psi \right)\leftrightarrow \left(\phi \to \psi \right)$$
7	6	orbi1i	$$⊢\left(\left(\neg \phi \vee \psi \right)\vee \neg \left(\phi \to \psi \right)\right)\leftrightarrow \left(\left(\phi \to \psi \right)\vee \neg \left(\phi \to \psi \right)\right)$$
8	1 7	mpbir	$$⊢\left(\left(\neg \phi \vee \psi \right)\vee \neg \left(\phi \to \psi \right)\right)$$
9	8	a1i	$$⊢\theta \to \left(\left(\neg \phi \vee \psi \right)\vee \neg \left(\phi \to \psi \right)\right)$$