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

Metamath Proof Explorer

Theorem oranabs

Description: Absorb a disjunct into a conjunct. (Contributed by Roy F. Longton, 23-Jun-2005) (Proof shortened by Wolf Lammen, 10-Nov-2013)

Ref Expression
Assertion oranabs ⊢ φ ∨ ¬ ψ ∧ ψ ↔ φ ∧ ψ

Proof

Step Hyp Ref Expression
1 biortn ⊢ ψ → φ ↔ ¬ ψ ∨ φ
2 orcom ⊢ ¬ ψ ∨ φ ↔ φ ∨ ¬ ψ
3 1 2 bitr2di ⊢ ψ → φ ∨ ¬ ψ ↔ φ
4 3 pm5.32ri ⊢ φ ∨ ¬ ψ ∧ ψ ↔ φ ∧ ψ