Metamath Proof Explorer

Theorem bj-andnotim

Description: Two ways of expressing a certain ternary connective. Note the respective positions of the three formulas on each side of the biconditional. (Contributed by BJ, 6-Oct-2018)

		Ref	Expression
	Assertion	bj-andnotim	$⊢ ((φ \land \neg ψ) \to χ) \leftrightarrow ((φ \to ψ) \lor χ)$

Proof

Step	Hyp	Ref	Expression
1		imor	$⊢ ((φ \land \neg ψ) \to χ) \leftrightarrow (\neg (φ \land \neg ψ) \lor χ)$
2		iman	$⊢ (φ \to ψ) \leftrightarrow \neg (φ \land \neg ψ)$
3	2	biimpri	$⊢ \neg (φ \land \neg ψ) \to (φ \to ψ)$
4	3	orim1i	$⊢ (\neg (φ \land \neg ψ) \lor χ) \to ((φ \to ψ) \lor χ)$
5	1 4	sylbi	$⊢ ((φ \land \neg ψ) \to χ) \to ((φ \to ψ) \lor χ)$
6		pm2.24	$⊢ ψ \to (\neg ψ \to χ)$
7	6	imim2i	$⊢ (φ \to ψ) \to (φ \to (\neg ψ \to χ))$
8	7	impd	$⊢ (φ \to ψ) \to ((φ \land \neg ψ) \to χ)$
9		ax-1	$⊢ χ \to ((φ \land \neg ψ) \to χ)$
10	8 9	jaoi	$⊢ ((φ \to ψ) \lor χ) \to ((φ \land \neg ψ) \to χ)$
11	5 10	impbii	$⊢ ((φ \land \neg ψ) \to χ) \leftrightarrow ((φ \to ψ) \lor χ)$