iscnrm3lem5

	Ref	Expression
Hypotheses	iscnrm3lem5.1	$⊢ (x = S \land y = T) \to (φ \leftrightarrow ψ)$
	iscnrm3lem5.2	$⊢ (x = S \land y = T) \to (χ \leftrightarrow θ)$
	iscnrm3lem5.3	$⊢ (τ \land η \land ζ) \to (S \in V \land T \in W)$
	iscnrm3lem5.4	$⊢ (τ \land η \land ζ) \to ((ψ \to θ) \to σ)$
Assertion	iscnrm3lem5	$⊢ τ \to (\forall x \in V \forall y \in W (φ \to χ) \to (η \to (ζ \to σ)))$

Step	Hyp	Ref	Expression
1		iscnrm3lem5.1	$⊢ (x = S \land y = T) \to (φ \leftrightarrow ψ)$
2		iscnrm3lem5.2	$⊢ (x = S \land y = T) \to (χ \leftrightarrow θ)$
3		iscnrm3lem5.3	$⊢ (τ \land η \land ζ) \to (S \in V \land T \in W)$
4		iscnrm3lem5.4	$⊢ (τ \land η \land ζ) \to ((ψ \to θ) \to σ)$
5	1 2	imbi12d	$⊢ (x = S \land y = T) \to ((φ \to χ) \leftrightarrow (ψ \to θ))$
6	5	rspc2gv	$⊢ (S \in V \land T \in W) \to (\forall x \in V \forall y \in W (φ \to χ) \to (ψ \to θ))$
7	6 3 4	iscnrm3lem4	$⊢ τ \to (\forall x \in V \forall y \in W (φ \to χ) \to (η \to (ζ \to σ)))$

Metamath Proof Explorer