Theorem iff_elimr ≪ | index | src | ≫

\iff逆消除

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

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

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)