Theorem tsbi3

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

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

Proof

Step	Hyp	Ref	Expression
1		biimpr	$$⊢\left(\phi \leftrightarrow \psi \right)\to \left(\psi \to \phi \right)$$
2		con34b	$$⊢\left(\psi \to \phi \right)\leftrightarrow \left(\neg \phi \to \neg \psi \right)$$
3		pm2.54	$$⊢\left(\neg \phi \to \neg \psi \right)\to \left(\phi \vee \neg \psi \right)$$
4	2 3	sylbi	$$⊢\left(\psi \to \phi \right)\to \left(\phi \vee \neg \psi \right)$$
5	1 4	syl	$$⊢\left(\phi \leftrightarrow \psi \right)\to \left(\phi \vee \neg \psi \right)$$
6	5	con3i	$$⊢\neg \left(\phi \vee \neg \psi \right)\to \neg \left(\phi \leftrightarrow \psi \right)$$
7	6	orri	$$⊢\left(\left(\phi \vee \neg \psi \right)\vee \neg \left(\phi \leftrightarrow \psi \right)\right)$$
8	7	a1i	$$⊢\theta \to \left(\left(\phi \vee \neg \psi \right)\vee \neg \left(\phi \leftrightarrow \psi \right)\right)$$