Metamath Proof Explorer

Theorem bnj642

Description: /\ -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Assertion bnj642 ⊢ φ ∧ ψ ∧ χ ∧ θ → φ

Proof

Step Hyp Ref Expression
1 bnj446 ⊢ φ ∧ ψ ∧ χ ∧ θ ↔ ψ ∧ χ ∧ θ ∧ φ
2 1 simprbi ⊢ φ ∧ ψ ∧ χ ∧ θ → φ