Theorem imp_iff_tran_imp ≪ | index | src | ≫

\imp\iff传递至\imp

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

Step	Hyp	Ref	Expression
1		imp_tran	(A \imp B) \imp (B \imp C) \imp A \imp C
2	1	_hyp_null_complete	(A \imp B) \and (B \iff C) \imp (A \imp B) \imp (B \imp C) \imp A \imp C
3		_hyp_null_intro	(A \imp B) \imp A \imp B
4	3	_hyp_complete	(A \imp B) \and (B \iff C) \imp A \imp B
5	2, 4	_hyp_mp	(A \imp B) \and (B \iff C) \imp (B \imp C) \imp A \imp C
6		iff_decomp	(B \iff C) \imp B \imp C
7	6	_hyp_null_complete	(A \imp B) \and (B \iff C) \imp (B \iff C) \imp B \imp C
8		_hyp_intro	(A \imp B) \and (B \iff C) \imp (B \iff C)
9	7, 8	_hyp_mp	(A \imp B) \and (B \iff C) \imp B \imp C
10	5, 9	_hyp_mp	(A \imp B) \and (B \iff C) \imp A \imp C
11	10	_hyp_rm	(A \imp B) \imp (B \iff C) \imp A \imp C

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)