Theorem bian2a | index | src |

theorem bian2a (a b: wff): $ (a -> b) -> (a /\ b <-> a) $;
StepHypRefExpression
1 anl
a /\ b -> a
2 1 a1i
(a -> b) -> a /\ b -> a
3 ian
a -> b -> a /\ b
4 3 a2i
(a -> b) -> a -> a /\ b
5 2, 4 ibid
(a -> b) -> (a /\ b <-> a)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)