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
|- ( ( ( ( ch /\ ps ) /\ ph ) /\ th ) -> ta )
Assertion 4an31
|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ta )

Proof

Step Hyp Ref Expression
1 4an31.1
 |-  ( ( ( ( ch /\ ps ) /\ ph ) /\ th ) -> ta )
2 an31
 |-  ( ( ( ph /\ ps ) /\ ch ) <-> ( ( ch /\ ps ) /\ ph ) )
3 2 1 sylanb
 |-  ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ta )