Theorem iff_intror_and ≪ | index | src | ≫

\iff右引入\and

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

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)