Theorem orfa

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

	Ref	Expression
Assertion	orfa	⊢ ( ( 𝜑 ∨ ⊥ ) ↔ 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		orcom	⊢ ( ( 𝜑 ∨ ⊥ ) ↔ ( ⊥ ∨ 𝜑 ) )
2		df-or	⊢ ( ( ⊥ ∨ 𝜑 ) ↔ ( ¬ ⊥ → 𝜑 ) )
3	1 2	bitri	⊢ ( ( 𝜑 ∨ ⊥ ) ↔ ( ¬ ⊥ → 𝜑 ) )
4		fal	⊢ ¬ ⊥
5		pm2.27	⊢ ( ¬ ⊥ → ( ( ¬ ⊥ → 𝜑 ) → 𝜑 ) )
6	4 5	ax-mp	⊢ ( ( ¬ ⊥ → 𝜑 ) → 𝜑 )
7	3 6	sylbi	⊢ ( ( 𝜑 ∨ ⊥ ) → 𝜑 )
8		orc	⊢ ( 𝜑 → ( 𝜑 ∨ ⊥ ) )
9	7 8	impbii	⊢ ( ( 𝜑 ∨ ⊥ ) ↔ 𝜑 )