Theorem iff_introl_or ≪ | index | src | ≫

\iff左引入\or

theorem iff_introl_or (A B C: wff): $ (B \iff C) \imp (A \or B \iff A \or C) $;
StepHypRefExpression
1 iff_simintro_or 
(A \iff A) \imp (B \iff C) \imp (A \or B \iff A \or C)
2 iff_refl 
A \iff A
3 1, 2 ax_mp 
(B \iff C) \imp (A \or B \iff A \or C)

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)