Metamath Proof Explorer

Theorem sbanALT

Description: Alternate version of sban . (Contributed by NM, 14-May-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.an	$⊢ η \leftrightarrow ((x = y \to (φ \land ψ)) \land \exists x (x = y \land (φ \land ψ)))$
	Assertion	sbanALT	$⊢ η \leftrightarrow (θ \land τ)$

Proof

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.an	$⊢ η \leftrightarrow ((x = y \to (φ \land ψ)) \land \exists x (x = y \land (φ \land ψ)))$
4		biid	$⊢ ((x = y \to (φ \to \neg ψ)) \land \exists x (x = y \land (φ \to \neg ψ))) \leftrightarrow ((x = y \to (φ \to \neg ψ)) \land \exists x (x = y \land (φ \to \neg ψ)))$
5		biid	$⊢ ((x = y \to \neg (φ \to \neg ψ)) \land \exists x (x = y \land \neg (φ \to \neg ψ))) \leftrightarrow ((x = y \to \neg (φ \to \neg ψ)) \land \exists x (x = y \land \neg (φ \to \neg ψ)))$
6	4 5	sbnALT	$⊢ ((x = y \to \neg (φ \to \neg ψ)) \land \exists x (x = y \land \neg (φ \to \neg ψ))) \leftrightarrow \neg ((x = y \to (φ \to \neg ψ)) \land \exists x (x = y \land (φ \to \neg ψ)))$
7		biid	$⊢ ((x = y \to \neg ψ) \land \exists x (x = y \land \neg ψ)) \leftrightarrow ((x = y \to \neg ψ) \land \exists x (x = y \land \neg ψ))$
8	1 7 4	sbimALT	$⊢ ((x = y \to (φ \to \neg ψ)) \land \exists x (x = y \land (φ \to \neg ψ))) \leftrightarrow (θ \to ((x = y \to \neg ψ) \land \exists x (x = y \land \neg ψ)))$
9	2 7	sbnALT	$⊢ ((x = y \to \neg ψ) \land \exists x (x = y \land \neg ψ)) \leftrightarrow \neg τ$
10	9	imbi2i	$⊢ (θ \to ((x = y \to \neg ψ) \land \exists x (x = y \land \neg ψ))) \leftrightarrow (θ \to \neg τ)$
11	8 10	bitri	$⊢ ((x = y \to (φ \to \neg ψ)) \land \exists x (x = y \land (φ \to \neg ψ))) \leftrightarrow (θ \to \neg τ)$
12	6 11	xchbinx	$⊢ ((x = y \to \neg (φ \to \neg ψ)) \land \exists x (x = y \land \neg (φ \to \neg ψ))) \leftrightarrow \neg (θ \to \neg τ)$
13		df-an	$⊢ (φ \land ψ) \leftrightarrow \neg (φ \to \neg ψ)$
14	3 5 13	sbbiiALT	$⊢ η \leftrightarrow ((x = y \to \neg (φ \to \neg ψ)) \land \exists x (x = y \land \neg (φ \to \neg ψ)))$
15		df-an	$⊢ (θ \land τ) \leftrightarrow \neg (θ \to \neg τ)$
16	12 14 15	3bitr4i	$⊢ η \leftrightarrow (θ \land τ)$