Metamath Proof Explorer

Theorem exp12bd

Description: The import-export theorem ( impexp ) for biconditionals (deduction form). (Contributed by Zhi Wang, 3-Sep-2024)

		Ref	Expression
	Hypothesis	exp12bd.1	$⊢ φ \to (((ψ \land χ) \to θ) \leftrightarrow ((τ \land η) \to ζ))$
	Assertion	exp12bd	$⊢ φ \to ((ψ \to (χ \to θ)) \leftrightarrow (τ \to (η \to ζ)))$

Step	Hyp	Ref	Expression
1		exp12bd.1	$⊢ φ \to (((ψ \land χ) \to θ) \leftrightarrow ((τ \land η) \to ζ))$
2		impexp	$⊢ ((ψ \land χ) \to θ) \leftrightarrow (ψ \to (χ \to θ))$
3		impexp	$⊢ ((τ \land η) \to ζ) \leftrightarrow (τ \to (η \to ζ))$
4	1 2 3	3bitr3g	$⊢ φ \to ((ψ \to (χ \to θ)) \leftrightarrow (τ \to (η \to ζ)))$