Theorem iff_eliml ≪ | index | src | ≫

\iff正消除

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

Step	Hyp	Ref	Expression
1		iff_decomp	(A \iff B) \imp A \imp B

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)