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

Metamath Proof Explorer

Theorem biort

Description: A disjunction with a true formula is equivalent to that true formula. (Contributed by NM, 23-May-1999)

Ref Expression
Assertion biort ⊢ φ → φ ↔ φ ∨ ψ

Proof

Step Hyp Ref Expression
1 id ⊢ φ → φ
2 orc ⊢ φ → φ ∨ ψ
3 1 2 2thd ⊢ φ → φ ↔ φ ∨ ψ