orfa

Description: The falsum F. can be removed from a disjunction. (Contributed by Giovanni Mascellani, 15-Sep-2017)

		Ref	Expression
	Assertion	orfa	$⊢ (φ \lor ⊥) \leftrightarrow φ$

Step	Hyp	Ref	Expression
1		orcom	$⊢ (φ \lor ⊥) \leftrightarrow (⊥ \lor φ)$
2		df-or	$⊢ (⊥ \lor φ) \leftrightarrow (\neg ⊥ \to φ)$
3	1 2	bitri	$⊢ (φ \lor ⊥) \leftrightarrow (\neg ⊥ \to φ)$
4		fal	$⊢ \neg ⊥$
5		pm2.27	$⊢ \neg ⊥ \to ((\neg ⊥ \to φ) \to φ)$
6	4 5	ax-mp	$⊢ (\neg ⊥ \to φ) \to φ$
7	3 6	sylbi	$⊢ (φ \lor ⊥) \to φ$
8		orc	$⊢ φ \to (φ \lor ⊥)$
9	7 8	impbii	$⊢ (φ \lor ⊥) \leftrightarrow φ$

Metamath Proof Explorer