| ⊢ (skip ∧ T) ⊃ (skip ⊃ T) | DfSkipAndNLoneImpBfSkipImpNLone |
Proof:
1 | (skip ∧ T) ≡more ∧ T | |
2 | (skip ∧¬T) ≡more ∧¬T | |
3 | more ∧ T ⊃ ¬(more ∧ T) | |
4 | (skip ∧ T) ⊃ ¬ (skip ∧¬T) | |
5 | skip ∧¬T ≡¬(skip ⊃ T) | |
6 | (skip ∧¬T) ≡¬(skip ⊃ T) | |
7 | ¬ (skip ∧¬T) ≡¬¬(skip ⊃ T) | |
8 | (skip ∧ T) ⊃ ¬¬(skip ⊃ T) | |
9 | (skip ∧ T) ⊃ (skip ⊃ T) | 8, def. of |
qed