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

Metamath Proof Explorer

Theorem biorfri

Description: A wff is equivalent to its disjunction with falsehood. (Contributed by NM, 23-Mar-1995) (Proof shortened by Wolf Lammen, 16-Jul-2021) (Proof shortened by AV, 10-Aug-2025)

Ref Expression
Hypothesis biorfi.1 ⊢ ¬ φ
Assertion biorfri ⊢ ψ ↔ ψ ∨ φ

Proof

Step Hyp Ref Expression
1 biorfi.1 ⊢ ¬ φ
2 1 biorfi ⊢ ψ ↔ φ ∨ ψ
3 orcom ⊢ φ ∨ ψ ↔ ψ ∨ φ
4 2 3 bitri ⊢ ψ ↔ ψ ∨ φ