Metamath Proof Explorer

Theorem 3anandis

Description: Inference that undistributes a triple conjunction in the antecedent. (Contributed by NM, 18-Apr-2007)

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


Step Hyp Ref Expression
1 3anandis.1 φ ψ φ χ φ θ τ
2 simpl φ ψ χ θ φ
3 simpr1 φ ψ χ θ ψ
4 simpr2 φ ψ χ θ χ
5 simpr3 φ ψ χ θ θ
6 2 3 2 4 2 5 1 syl222anc φ ψ χ θ τ