ichim

Description: Formula building rule for implication in interchangeability. (Contributed by SN, 4-May-2024)

		Ref	Expression
	Assertion	ichim	$⊢ ([a ⇄ b] φ \land [a ⇄ b] ψ) \to [a ⇄ b] (φ \to ψ)$

Step	Hyp	Ref	Expression
1		ichn	$⊢ [a ⇄ b] ψ \leftrightarrow [a ⇄ b] \neg ψ$
2		ichan	$⊢ ([a ⇄ b] φ \land [a ⇄ b] \neg ψ) \to [a ⇄ b] (φ \land \neg ψ)$
3	1 2	sylan2b	$⊢ ([a ⇄ b] φ \land [a ⇄ b] ψ) \to [a ⇄ b] (φ \land \neg ψ)$
4		ichn	$⊢ [a ⇄ b] (φ \land \neg ψ) \leftrightarrow [a ⇄ b] \neg (φ \land \neg ψ)$
5	3 4	sylib	$⊢ ([a ⇄ b] φ \land [a ⇄ b] ψ) \to [a ⇄ b] \neg (φ \land \neg ψ)$
6		iman	$⊢ (φ \to ψ) \leftrightarrow \neg (φ \land \neg ψ)$
7	6	a1i	$⊢ ⊤ \to ((φ \to ψ) \leftrightarrow \neg (φ \land \neg ψ))$
8	7	ichbidv	$⊢ ⊤ \to ([a ⇄ b] (φ \to ψ) \leftrightarrow [a ⇄ b] \neg (φ \land \neg ψ))$
9	8	mptru	$⊢ [a ⇄ b] (φ \to ψ) \leftrightarrow [a ⇄ b] \neg (φ \land \neg ψ)$
10	5 9	sylibr	$⊢ ([a ⇄ b] φ \land [a ⇄ b] ψ) \to [a ⇄ b] (φ \to ψ)$

Metamath Proof Explorer