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

Metamath Proof Explorer

Theorem pm2.24nel

Description: A contradiction concerning membership implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018)

		Ref	Expression
	Assertion	pm2.24nel	$⊢ A \in B \to (A \notin B \to φ)$

Step	Hyp	Ref	Expression
1		df-nel	$⊢ A \notin B \leftrightarrow \neg A \in B$
2		pm2.24	$⊢ A \in B \to (\neg A \in B \to φ)$
3	1 2	biimtrid	$⊢ A \in B \to (A \notin B \to φ)$