Metamath Proof Explorer


Theorem an4s

Description: Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995)

Ref Expression
Hypothesis an4s.1 φ ψ χ θ τ
Assertion an4s φ χ ψ θ τ

Proof

Step Hyp Ref Expression
1 an4s.1 φ ψ χ θ τ
2 an4 φ χ ψ θ φ ψ χ θ
3 2 1 sylbi φ χ ψ θ τ