sblbisALT

Description: Alternate version of sblbis . (Contributed by NM, 19-Aug-1993) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dfsb1.p6	$⊢ θ \leftrightarrow ((x = y \to φ) \land \exists x (x = y \land φ))$
	dfsb1.s4	$⊢ τ \leftrightarrow ((x = y \to ψ) \land \exists x (x = y \land ψ))$
	dfsb1.bi	$⊢ η \leftrightarrow ((x = y \to (φ \leftrightarrow ψ)) \land \exists x (x = y \land (φ \leftrightarrow ψ)))$
	sblbisALT.1	$⊢ τ \leftrightarrow χ$
Assertion	sblbisALT	$⊢ η \leftrightarrow (θ \leftrightarrow χ)$

Step	Hyp	Ref	Expression
1		dfsb1.p6	$⊢ θ \leftrightarrow ((x = y \to φ) \land \exists x (x = y \land φ))$
2		dfsb1.s4	$⊢ τ \leftrightarrow ((x = y \to ψ) \land \exists x (x = y \land ψ))$
3		dfsb1.bi	$⊢ η \leftrightarrow ((x = y \to (φ \leftrightarrow ψ)) \land \exists x (x = y \land (φ \leftrightarrow ψ)))$
4		sblbisALT.1	$⊢ τ \leftrightarrow χ$
5	1 2 3	sbbiALT	$⊢ η \leftrightarrow (θ \leftrightarrow τ)$
6	4	bibi2i	$⊢ (θ \leftrightarrow τ) \leftrightarrow (θ \leftrightarrow χ)$
7	5 6	bitri	$⊢ η \leftrightarrow (θ \leftrightarrow χ)$

Metamath Proof Explorer