sbi2ALT

Description: Alternate version of sbi2 . (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	sbi2ALT	$⊢ (θ \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		biid	$⊢ ((x = y \to \neg φ) \land \exists x (x = y \land \neg φ)) \leftrightarrow ((x = y \to \neg φ) \land \exists x (x = y \land \neg φ))$
5	1 4	sbnALT	$⊢ ((x = y \to \neg φ) \land \exists x (x = y \land \neg φ)) \leftrightarrow \neg θ$
6		pm2.21	$⊢ \neg φ \to (φ \to ψ)$
7	4 3 6	sbimiALT	$⊢ ((x = y \to \neg φ) \land \exists x (x = y \land \neg φ)) \to η$
8	5 7	sylbir	$⊢ \neg θ \to η$
9		ax-1	$⊢ ψ \to (φ \to ψ)$
10	2 3 9	sbimiALT	$⊢ τ \to η$
11	8 10	ja	$⊢ (θ \to τ) \to η$

Metamath Proof Explorer