Theorem mp_with_ant_thm ≪ | index | src | ≫

带前件的MP公式

theorem mp_with_ant_thm (A B C: wff):
  $ (A \imp B \imp C) \imp (A \imp B) \imp A \imp C $;

Step	Hyp	Ref	Expression
1		imp_imp_insl	(A \imp B \imp C) \imp (A \imp B) \imp A \imp C

Axiom use

Logic (ax_2)