\and右拆分
theorem and_splitr (A B: wff): $ A \and B \imp B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | neg_imp_swap | (\neg B \imp A \imp \neg B) \imp \neg (A \imp \neg B) \imp B |
|
| 2 | introl_imp | \neg B \imp A \imp \neg B |
|
| 3 | 1, 2 | ax_mp | \neg (A \imp \neg B) \imp B |
| 4 | 3 | conv and | A \and B \imp B |