∧右拆分
theorem and_right_split (A B: wff): $ A \and B \imp B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imp_left_neg_permute | (\neg B \imp A \imp \neg B) \imp \neg (A \imp \neg B) \imp B |
|
| 2 | imp_left_intro | \neg B \imp A \imp \neg B |
|
| 3 | 1, 2 | mp | \neg (A \imp \neg B) \imp B |
| 4 | 3 | conv and | A \and B \imp B |