This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj1101

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

Step	Hyp	Ref	Expression
1		bnj1101.1	$⊢ \exists x (φ \to ψ)$
2		bnj1101.2	$⊢ χ \to φ$
3		pm3.42	$⊢ (φ \to ψ) \to ((χ \land φ) \to ψ)$
4	1 3	bnj101	$⊢ \exists x ((χ \land φ) \to ψ)$
5	2	pm4.71i	$⊢ χ \leftrightarrow (χ \land φ)$
6	5	imbi1i	$⊢ (χ \to ψ) \leftrightarrow ((χ \land φ) \to ψ)$
7	6	exbii	$⊢ \exists x (χ \to ψ) \leftrightarrow \exists x ((χ \land φ) \to ψ)$
8	4 7	mpbir	$⊢ \exists x (χ \to ψ)$