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

Metamath Proof Explorer

Theorem anabs7

Description: Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996) (Proof shortened by Wolf Lammen, 17-Nov-2013)

Ref Expression
Assertion anabs7 ⊢ ψ ∧ φ ∧ ψ ↔ φ ∧ ψ

Proof

Step Hyp Ref Expression
1 simpr ⊢ φ ∧ ψ → ψ
2 1 pm4.71ri ⊢ φ ∧ ψ ↔ ψ ∧ φ ∧ ψ
3 2 bicomi ⊢ ψ ∧ φ ∧ ψ ↔ φ ∧ ψ