sbi1ALT

Description: Alternate version of sbi1 . (Contributed by NM, 14-May-1993) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dfsb1.p5	$⊢ θ \leftrightarrow ((x = y \to φ) \land \exists x (x = y \land φ))$
	dfsb1.s2	$⊢ τ \leftrightarrow ((x = y \to ψ) \land \exists x (x = y \land ψ))$
	dfsb1.im	$⊢ η \leftrightarrow ((x = y \to (φ \to ψ)) \land \exists x (x = y \land (φ \to ψ)))$
Assertion	sbi1ALT	$⊢ η \to (θ \to τ)$

Step	Hyp	Ref	Expression
1		dfsb1.p5	$⊢ θ \leftrightarrow ((x = y \to φ) \land \exists x (x = y \land φ))$
2		dfsb1.s2	$⊢ τ \leftrightarrow ((x = y \to ψ) \land \exists x (x = y \land ψ))$
3		dfsb1.im	$⊢ η \leftrightarrow ((x = y \to (φ \to ψ)) \land \exists x (x = y \land (φ \to ψ)))$
4	1	sbequ2ALT	$⊢ x = y \to (θ \to φ)$
5	3	sbequ2ALT	$⊢ x = y \to (η \to (φ \to ψ))$
6	4 5	syl5d	$⊢ x = y \to (η \to (θ \to ψ))$
7	2	sbequ1ALT	$⊢ x = y \to (ψ \to τ)$
8	6 7	syl6d	$⊢ x = y \to (η \to (θ \to τ))$
9	8	sps	$⊢ \forall x x = y \to (η \to (θ \to τ))$
10	1	sb4ALT	$⊢ \neg \forall x x = y \to (θ \to \forall x (x = y \to φ))$
11	3	sb4ALT	$⊢ \neg \forall x x = y \to (η \to \forall x (x = y \to (φ \to ψ)))$
12		ax-2	$⊢ (x = y \to (φ \to ψ)) \to ((x = y \to φ) \to (x = y \to ψ))$
13	12	al2imi	$⊢ \forall x (x = y \to (φ \to ψ)) \to (\forall x (x = y \to φ) \to \forall x (x = y \to ψ))$
14	2	sb2ALT	$⊢ \forall x (x = y \to ψ) \to τ$
15	13 14	syl6	$⊢ \forall x (x = y \to (φ \to ψ)) \to (\forall x (x = y \to φ) \to τ)$
16	11 15	syl6	$⊢ \neg \forall x x = y \to (η \to (\forall x (x = y \to φ) \to τ))$
17	10 16	syl5d	$⊢ \neg \forall x x = y \to (η \to (θ \to τ))$
18	9 17	pm2.61i	$⊢ η \to (θ \to τ)$

Metamath Proof Explorer