Theorem imp_reflect ≪ | index | src | ≫

同一律

theorem imp_reflect (A: wff): $ A \imp A $;


(A \imp (A \imp A) \imp A) \imp (A \imp A \imp A) \imp A \imp A
A \imp (A \imp A) \imp A
(A \imp A \imp A) \imp A \imp A
A \imp A \imp A
A \imp A

Step	Hyp	Ref	Expression
1		imp_for_imp_left_insert	(A \imp (A \imp A) \imp A) \imp (A \imp A \imp A) \imp A \imp A
2		imp_left_intro	A \imp (A \imp A) \imp A
3	1, 2	mp	(A \imp A \imp A) \imp A \imp A
4		imp_left_intro	A \imp A \imp A
5	3, 4	mp	A \imp A

Axiom use

ZFC (ax_mp, ax_p1, ax_p2)