Description: Deduction eliminating disjunct. (Contributed by Thierry Arnoux, 19-Dec-2016)
Ref | Expression | ||
---|---|---|---|
Hypothesis | 3o1cs.1 | |- ( ( ph \/ ps \/ ch ) -> th ) |
|
Assertion | 3o1cs | |- ( ph -> th ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3o1cs.1 | |- ( ( ph \/ ps \/ ch ) -> th ) |
|
2 | df-3or | |- ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) ) |
|
3 | 2 1 | sylbir | |- ( ( ( ph \/ ps ) \/ ch ) -> th ) |
4 | 3 | orcs | |- ( ( ph \/ ps ) -> th ) |
5 | 4 | orcs | |- ( ph -> th ) |