Theorem iff_introl_and ≪ | index | src | ≫

\iff左引入\and

theorem iff_introl_and (A B C: wff):
  $ (B \iff C) \imp (A \and B \iff A \and C) $;
StepHypRefExpression
1 iff_simintro_and 
(A \iff A) \imp (B \iff C) \imp (A \and B \iff A \and C)
2 iff_refl 
A \iff A
3 1, 2 ax_mp 
(B \iff C) \imp (A \and B \iff A \and C)

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)