Metamath Proof Explorer

Theorem anandis

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

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


Step Hyp Ref Expression
1 anandis.1 φ ψ φ χ τ
2 1 an4s φ φ ψ χ τ
3 2 anabsan φ ψ χ τ