ifpnOLD

Description: Obsolete version of ifpn as of 5-May-2024. (Contributed by BJ, 30-Sep-2019) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	ifpnOLD	$⊢ if- (φ, ψ, χ) \leftrightarrow if- (\neg φ, χ, ψ)$

Proof

Step	Hyp	Ref	Expression
1		notnotb	$⊢ φ \leftrightarrow \neg \neg φ$
2	1	imbi1i	$⊢ (φ \to ψ) \leftrightarrow (\neg \neg φ \to ψ)$
3	2	anbi2ci	$⊢ ((φ \to ψ) \land (\neg φ \to χ)) \leftrightarrow ((\neg φ \to χ) \land (\neg \neg φ \to ψ))$
4		dfifp2	$⊢ if- (φ, ψ, χ) \leftrightarrow ((φ \to ψ) \land (\neg φ \to χ))$
5		dfifp2	$⊢ if- (\neg φ, χ, ψ) \leftrightarrow ((\neg φ \to χ) \land (\neg \neg φ \to ψ))$
6	3 4 5	3bitr4i	$⊢ if- (φ, ψ, χ) \leftrightarrow if- (\neg φ, χ, ψ)$

Metamath Proof Explorer

Theorem ifpnOLD

Proof