Description: If the second and third disjuncts of a true triple disjunction are false, then the first disjunct is true. Automatically derived from 3ornot23VD . (Contributed by Alan Sare, 31-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 3ornot23 | |- ( ( -. ph /\ -. ps ) -> ( ( ch \/ ph \/ ps ) -> ch ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | idd | |- ( -. ph -> ( ch -> ch ) ) |
|
| 2 | pm2.21 | |- ( -. ph -> ( ph -> ch ) ) |
|
| 3 | pm2.21 | |- ( -. ps -> ( ps -> ch ) ) |
|
| 4 | 1 2 3 | 3jaao | |- ( ( -. ph /\ -. ph /\ -. ps ) -> ( ( ch \/ ph \/ ps ) -> ch ) ) |
| 5 | 4 | 3anidm12 | |- ( ( -. ph /\ -. ps ) -> ( ( ch \/ ph \/ ps ) -> ch ) ) |