Metamath Proof Explorer


Theorem or4

Description: Rearrangement of 4 disjuncts. (Contributed by NM, 12-Aug-1994)

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

Proof

Step Hyp Ref Expression
1 or12
 |-  ( ( ps \/ ( ch \/ th ) ) <-> ( ch \/ ( ps \/ th ) ) )
2 1 orbi2i
 |-  ( ( ph \/ ( ps \/ ( ch \/ th ) ) ) <-> ( ph \/ ( ch \/ ( ps \/ th ) ) ) )
3 orass
 |-  ( ( ( ph \/ ps ) \/ ( ch \/ th ) ) <-> ( ph \/ ( ps \/ ( ch \/ th ) ) ) )
4 orass
 |-  ( ( ( ph \/ ch ) \/ ( ps \/ th ) ) <-> ( ph \/ ( ch \/ ( ps \/ th ) ) ) )
5 2 3 4 3bitr4i
 |-  ( ( ( ph \/ ps ) \/ ( ch \/ th ) ) <-> ( ( ph \/ ch ) \/ ( ps \/ th ) ) )