Metamath Proof Explorer


Theorem anandirs

Description: Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004)

Ref Expression
Hypothesis anandirs.1 φ χ ψ χ τ
Assertion anandirs φ ψ χ τ

Proof

Step Hyp Ref Expression
1 anandirs.1 φ χ ψ χ τ
2 1 an4s φ ψ χ χ τ
3 2 anabsan2 φ ψ χ τ