Metamath Proof Explorer

Theorem bnj1109

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	bnj1109.1	$⊢ \exists x ((A \neq B \land φ) \to ψ)$
		bnj1109.2	$⊢ (A = B \land φ) \to ψ$
	Assertion	bnj1109	$⊢ \exists x (φ \to ψ)$

Proof

Step	Hyp	Ref	Expression
1		bnj1109.1	$⊢ \exists x ((A \neq B \land φ) \to ψ)$
2		bnj1109.2	$⊢ (A = B \land φ) \to ψ$
3	2	ex	$⊢ A = B \to (φ \to ψ)$
4	3	a1i	$⊢ (A \neq B \to (φ \to ψ)) \to (A = B \to (φ \to ψ))$
5	4	ax-gen	$⊢ \forall x ((A \neq B \to (φ \to ψ)) \to (A = B \to (φ \to ψ)))$
6		impexp	$⊢ ((A \neq B \land φ) \to ψ) \leftrightarrow (A \neq B \to (φ \to ψ))$
7	6	exbii	$⊢ \exists x ((A \neq B \land φ) \to ψ) \leftrightarrow \exists x (A \neq B \to (φ \to ψ))$
8	1 7	mpbi	$⊢ \exists x (A \neq B \to (φ \to ψ))$
9		exintr	$⊢ \forall x ((A \neq B \to (φ \to ψ)) \to (A = B \to (φ \to ψ))) \to (\exists x (A \neq B \to (φ \to ψ)) \to \exists x ((A \neq B \to (φ \to ψ)) \land (A = B \to (φ \to ψ))))$
10	5 8 9	mp2	$⊢ \exists x ((A \neq B \to (φ \to ψ)) \land (A = B \to (φ \to ψ)))$
11		exancom	$⊢ \exists x ((A \neq B \to (φ \to ψ)) \land (A = B \to (φ \to ψ))) \leftrightarrow \exists x ((A = B \to (φ \to ψ)) \land (A \neq B \to (φ \to ψ)))$
12	10 11	mpbi	$⊢ \exists x ((A = B \to (φ \to ψ)) \land (A \neq B \to (φ \to ψ)))$
13		df-ne	$⊢ A \neq B \leftrightarrow \neg A = B$
14	13	imbi1i	$⊢ (A \neq B \to (φ \to ψ)) \leftrightarrow (\neg A = B \to (φ \to ψ))$
15		pm2.61	$⊢ (A = B \to (φ \to ψ)) \to ((\neg A = B \to (φ \to ψ)) \to (φ \to ψ))$
16	15	imp	$⊢ ((A = B \to (φ \to ψ)) \land (\neg A = B \to (φ \to ψ))) \to (φ \to ψ)$
17	14 16	sylan2b	$⊢ ((A = B \to (φ \to ψ)) \land (A \neq B \to (φ \to ψ))) \to (φ \to ψ)$
18	12 17	bnj101	$⊢ \exists x (φ \to ψ)$