Metamath Proof Explorer

Theorem an43

Description: Rearrangement of 4 conjuncts. (Contributed by Rodolfo Medina, 24-Sep-2010) (Proof shortened by Andrew Salmon, 29-Jun-2011)

Ref Expression
Assertion an43 
|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ( ph /\ th ) /\ ( ps /\ ch ) ) )

Proof

Step Hyp Ref Expression
1 an42 
 |-  ( ( ( ph /\ th ) /\ ( ps /\ ch ) ) <-> ( ( ph /\ ps ) /\ ( ch /\ th ) ) )
2 1 bicomi 
 |-  ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ( ph /\ th ) /\ ( ps /\ ch ) ) )