theorem iff_comp (A B: wff): $ (A \imp B) \imp (B \imp A) \imp (A \iff B) $;
| Step | Hyp | Ref | Expression |
|---|
| 1 |
|
and_comp |
(A \imp B) \imp (B \imp A) \imp (A \imp B) \and (B \imp A) |
| 2 |
1 |
conv iff |
(A \imp B) \imp (B \imp A) \imp (A \iff B) |
Axiom use
Logic
(ax_mp,
ax_1,
ax_2,
ax_3)