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 |
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 |