Metamath Proof Explorer

Theorem sbimALT

Description: Alternate version of sbim . (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	sbimALT	$⊢ η \leftrightarrow (θ \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 2 3	sbi1ALT	$⊢ η \to (θ \to τ)$
5	1 2 3	sbi2ALT	$⊢ (θ \to τ) \to η$
6	4 5	impbii	$⊢ η \leftrightarrow (θ \to τ)$