Metamath Proof Explorer

Theorem ifpdfbiOLD

Description: Obsolete version of ifpdfbi as of 25-Jun-2026. Define the biconditional as conditional logic operator. (Contributed by RP, 20-Apr-2020) (Proof shortened by Wolf Lammen, 30-Apr-2024) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		con34b	$⊢ (ψ \to φ) \leftrightarrow (\neg φ \to \neg ψ)$
2	1	anbi2i	$⊢ ((φ \to ψ) \land (ψ \to φ)) \leftrightarrow ((φ \to ψ) \land (\neg φ \to \neg ψ))$
3		dfbi2	$⊢ (φ \leftrightarrow ψ) \leftrightarrow ((φ \to ψ) \land (ψ \to φ))$
4		dfifp2	$⊢ if- (φ, ψ, \neg ψ) \leftrightarrow ((φ \to ψ) \land (\neg φ \to \neg ψ))$
5	2 3 4	3bitr4i	$⊢ (φ \leftrightarrow ψ) \leftrightarrow if- (φ, ψ, \neg ψ)$