Theorem or_and_distl ≪ | index | src | ≫

\or\and左分配

theorem or_and_distl (A B C: wff):
  $ A \or (B \and C) \iff A \or B \and (A \or C) $;
StepHypRefExpression
1 imp_and_distl 
\neg A \imp B \and C \iff (\neg A \imp B) \and (\neg A \imp C)
2 1 conv or 
A \or (B \and C) \iff A \or B \and (A \or C)

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)