Description: A rearrangement of disjuncts. (Contributed by NM, 18-Oct-1995) (Proof shortened by Andrew Salmon, 26-Jun-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | or32 | |- ( ( ( ph \/ ps ) \/ ch ) <-> ( ( ph \/ ch ) \/ ps ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orass | |- ( ( ( ph \/ ps ) \/ ch ) <-> ( ph \/ ( ps \/ ch ) ) ) |
|
2 | or12 | |- ( ( ph \/ ( ps \/ ch ) ) <-> ( ps \/ ( ph \/ ch ) ) ) |
|
3 | orcom | |- ( ( ps \/ ( ph \/ ch ) ) <-> ( ( ph \/ ch ) \/ ps ) ) |
|
4 | 1 2 3 | 3bitri | |- ( ( ( ph \/ ps ) \/ ch ) <-> ( ( ph \/ ch ) \/ ps ) ) |