Metamath Proof Explorer


Theorem 4an21

Description: Rearrangement of 4 conjuncts with a triple conjunction. (Contributed by AV, 4-Mar-2022)

Ref Expression
Assertion 4an21 φψχθψφχθ

Proof

Step Hyp Ref Expression
1 3anass φψχθφψχθ
2 ancom φψψφ
3 2 anbi1i φψχθψφχθ
4 anass ψφχθψφχθ
5 3anass φχθφχθ
6 5 bicomi φχθφχθ
7 6 anbi2i ψφχθψφχθ
8 4 7 bitri ψφχθψφχθ
9 3 8 bitri φψχθψφχθ
10 1 9 bitri φψχθψφχθ