Theorem itr ≪ | index | src

→传递规则

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


(A \imp B) \imp (B \imp C) \imp A \imp C
A \imp B
(B \imp C) \imp A \imp C
B \imp C
A \imp C

Step	Hyp	Ref	Expression
1		iirvi	(A \imp B) \imp (B \imp C) \imp A \imp C
2		hyp h1	A \imp B
3	1, 2	mp	(B \imp C) \imp A \imp C
4		hyp h2	B \imp C
5	3, 4	mp	A \imp C

Axiom use

ZFC (ax_mp, ax_p1, ax_p2)