Description: A rearrangement of disjuncts, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018)
Ref | Expression | ||
---|---|---|---|
Hypothesis | or32dd.1 | |- ( ph -> ( ps -> ( ( ch \/ th ) \/ ta ) ) ) |
|
Assertion | or32dd | |- ( ph -> ( ps -> ( ( ch \/ ta ) \/ th ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | or32dd.1 | |- ( ph -> ( ps -> ( ( ch \/ th ) \/ ta ) ) ) |
|
2 | or32 | |- ( ( ( ch \/ ta ) \/ th ) <-> ( ( ch \/ th ) \/ ta ) ) |
|
3 | 1 2 | syl6ibr | |- ( ph -> ( ps -> ( ( ch \/ ta ) \/ th ) ) ) |