∧合成
theorem and_compound (A B: wff): $ A \imp B \imp A \and B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imp_trans_curried | (A \imp (A \imp \neg B) \imp \neg B) \imp (((A \imp \neg B) \imp \neg B) \imp B \imp \neg (A \imp \neg B)) \imp A \imp B \imp \neg (A \imp \neg B) |
|
| 2 | imp_for_imp_left_permute | ((A \imp \neg B) \imp A \imp \neg B) \imp A \imp (A \imp \neg B) \imp \neg B |
|
| 3 | imp_reflect | (A \imp \neg B) \imp A \imp \neg B |
|
| 4 | 2, 3 | mp | A \imp (A \imp \neg B) \imp \neg B |
| 5 | 1, 4 | mp | (((A \imp \neg B) \imp \neg B) \imp B \imp \neg (A \imp \neg B)) \imp A \imp B \imp \neg (A \imp \neg B) |
| 6 | imp_right_neg_permute | ((A \imp \neg B) \imp \neg B) \imp B \imp \neg (A \imp \neg B) |
|
| 7 | 5, 6 | mp | A \imp B \imp \neg (A \imp \neg B) |
| 8 | 7 | conv and | A \imp B \imp A \and B |