Metamath Proof Explorer


Theorem 4an31

Description: A rearrangement of conjuncts for a 4-right-nested conjunction. (Contributed by Alan Sare, 30-May-2018)

Ref Expression
Hypothesis 4an31.1 χ ψ φ θ τ
Assertion 4an31 φ ψ χ θ τ

Proof

Step Hyp Ref Expression
1 4an31.1 χ ψ φ θ τ
2 an31 φ ψ χ χ ψ φ
3 2 1 sylanb φ ψ χ θ τ