Theorem iff_decomp ≪ | index | src | ≫

\iff正分解

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

Step	Hyp	Ref	Expression
1		and_splitl	(A \imp B) \and (B \imp A) \imp A \imp B
2	1	conv iff	(A \iff B) \imp A \imp B

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)