Theorem iff_introl_iff ≪ | index | src | ≫

\iff左引入\iff

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

Step	Hyp	Ref	Expression
1		iff_simintro_iff	(A \iff A) \imp (B \iff C) \imp ((A \iff B) \iff A \iff C)
2		iff_refl	A \iff A
3	1, 2	ax_mp	(B \iff C) \imp ((A \iff B) \iff A \iff C)

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)