Theorem iff_decompbwd ≪ | index | src | ≫

\iff逆分解

theorem iff_decompbwd (A B: wff): $ (A \iff B) \imp B \imp A $;
StepHypRefExpression
1 and_splitr 
(A \imp B) \and (B \imp A) \imp B \imp A
2 1 conv iff 
(A \iff B) \imp B \imp A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)