Description: If a double conjunction is false and the second conjunct is true, then the first conjunct is false. https://us.metamath.org/other/completeusersproof/not12an2impnot1vd.html is the Virtual Deduction proof verified by automatically transforming it into the Metamath proof of not12an2impnot1 using completeusersproof, which is verified by the Metamath program. https://us.metamath.org/other/completeusersproof/not12an2impnot1ro.html is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. (Contributed by Alan Sare, 13-Jun-2018)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | not12an2impnot1 | |- ( ( -. ( ph /\ ps ) /\ ps ) -> -. ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pm3.21 | |- ( ps -> ( ph -> ( ph /\ ps ) ) ) |
|
| 2 | 1 | con3rr3 | |- ( -. ( ph /\ ps ) -> ( ps -> -. ph ) ) |
| 3 | 2 | imp | |- ( ( -. ( ph /\ ps ) /\ ps ) -> -. ph ) |