ichbidv

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

		Ref	Expression
	Hypothesis	ichbidv.1	$⊢ φ \to (ψ \leftrightarrow χ)$
	Assertion	ichbidv	$⊢ φ \to ([x ⇄ y] ψ \leftrightarrow [x ⇄ y] χ)$

Step	Hyp	Ref	Expression
1		ichbidv.1	$⊢ φ \to (ψ \leftrightarrow χ)$
2	1	sbbidv	$⊢ φ \to ([a/ y] ψ \leftrightarrow [a/ y] χ)$
3	2	sbbidv	$⊢ φ \to ([y/ x] [a/ y] ψ \leftrightarrow [y/ x] [a/ y] χ)$
4	3	sbbidv	$⊢ φ \to ([x/ a] [y/ x] [a/ y] ψ \leftrightarrow [x/ a] [y/ x] [a/ y] χ)$
5	4 1	bibi12d	$⊢ φ \to (([x/ a] [y/ x] [a/ y] ψ \leftrightarrow ψ) \leftrightarrow ([x/ a] [y/ x] [a/ y] χ \leftrightarrow χ))$
6	5	albidv	$⊢ φ \to (\forall y ([x/ a] [y/ x] [a/ y] ψ \leftrightarrow ψ) \leftrightarrow \forall y ([x/ a] [y/ x] [a/ y] χ \leftrightarrow χ))$
7	6	albidv	$⊢ φ \to (\forall x \forall y ([x/ a] [y/ x] [a/ y] ψ \leftrightarrow ψ) \leftrightarrow \forall x \forall y ([x/ a] [y/ x] [a/ y] χ \leftrightarrow χ))$
8		df-ich	$⊢ [x ⇄ y] ψ \leftrightarrow \forall x \forall y ([x/ a] [y/ x] [a/ y] ψ \leftrightarrow ψ)$
9		df-ich	$⊢ [x ⇄ y] χ \leftrightarrow \forall x \forall y ([x/ a] [y/ x] [a/ y] χ \leftrightarrow χ)$
10	7 8 9	3bitr4g	$⊢ φ \to ([x ⇄ y] ψ \leftrightarrow [x ⇄ y] χ)$

Metamath Proof Explorer