Metamath Proof Explorer


Theorem biorfi

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

Ref Expression
Hypothesis biorfi.1 ¬φ
Assertion biorfi ψψφ

Proof

Step Hyp Ref Expression
1 biorfi.1 ¬φ
2 orc ψψφ
3 pm2.53 ψφ¬ψφ
4 1 3 mt3i ψφψ
5 2 4 impbii ψψφ