ts3an2

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

		Ref	Expression
	Assertion	ts3an2	$⊢ θ \to ((φ \land ψ) \lor \neg (φ \land ψ \land χ))$

Step	Hyp	Ref	Expression
1		tsan2	$⊢ θ \to ((φ \land ψ) \lor \neg ((φ \land ψ) \land χ))$
2		df-3an	$⊢ (φ \land ψ \land χ) \leftrightarrow ((φ \land ψ) \land χ)$
3	2	notbii	$⊢ \neg (φ \land ψ \land χ) \leftrightarrow \neg ((φ \land ψ) \land χ)$
4	3	orbi2i	$⊢ ((φ \land ψ) \lor \neg (φ \land ψ \land χ)) \leftrightarrow ((φ \land ψ) \lor \neg ((φ \land ψ) \land χ))$
5	1 4	sylibr	$⊢ θ \to ((φ \land ψ) \lor \neg (φ \land ψ \land χ))$

Metamath Proof Explorer