Description: Rearrangement of 4 disjuncts. (Contributed by NM, 12-Aug-1994)
Ref | Expression | ||
---|---|---|---|
Assertion | or4 | |- ( ( ( ph \/ ps ) \/ ( ch \/ th ) ) <-> ( ( ph \/ ch ) \/ ( ps \/ th ) ) ) |
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 ) ) ) |