Metamath Proof Explorer

Theorem logic2

Description: Variant of logic1 . (Contributed by Zhi Wang, 30-Aug-2024)

	Ref	Expression
Hypotheses	logic1.1	$⊢ φ \to (ψ \leftrightarrow χ)$
	logic2.2	$⊢ φ \to ((ψ \land χ) \to (θ \leftrightarrow τ))$
Assertion	logic2	$⊢ φ \to ((ψ \to θ) \leftrightarrow (χ \to τ))$

Step	Hyp	Ref	Expression
1		logic1.1	$⊢ φ \to (ψ \leftrightarrow χ)$
2		logic2.2	$⊢ φ \to ((ψ \land χ) \to (θ \leftrightarrow τ))$
3	1	pm4.71da	$⊢ φ \to (ψ \leftrightarrow (ψ \land χ))$
4	3 2	sylbid	$⊢ φ \to (ψ \to (θ \leftrightarrow τ))$
5	1 4	logic1	$⊢ φ \to ((ψ \to θ) \leftrightarrow (χ \to τ))$