Metamath Proof Explorer


Theorem 4an4132

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

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

Proof

Step Hyp Ref Expression
1 4an4132.1 θ χ ψ φ τ
2 simpr φ ψ χ θ θ
3 simplr φ ψ χ θ χ
4 2 3 jca φ ψ χ θ θ χ
5 simpllr φ ψ χ θ ψ
6 simplll φ ψ χ θ φ
7 4 5 6 1 syl21anc φ ψ χ θ τ