Theorem oreq2i | index | src |

theorem oreq2i (a b c: wff): $ b <-> c $ > $ a \/ b <-> a \/ c $;
StepHypRefExpression
1 id
(b <-> c) -> (b <-> c)
2 1 oreq2d
(b <-> c) -> (a \/ b <-> a \/ c)
3 hyp h
b <-> c
4 2, 3 ax_mp
a \/ b <-> a \/ c

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)