Theorem imp_nested_gatherl_and ≪ | index | src | ≫

嵌套前件收集\and

theorem imp_nested_gatherl_and (A B C: wff):
  $ A \imp B \imp C \iff A \and B \imp C $;
StepHypRefExpression
1 iff_comp 
((A \imp B \imp C) \imp A \and B \imp C) \imp ((A \and B \imp C) \imp A \imp B \imp C) \imp (A \imp B \imp C \iff A \and B \imp C)
2 imp_nested_assemb_and 
(A \imp B \imp C) \imp A \and B \imp C
3 1, 2 ax_mp 
((A \and B \imp C) \imp A \imp B \imp C) \imp (A \imp B \imp C \iff A \and B \imp C)
4 and_imp_break_nested 
(A \and B \imp C) \imp A \imp B \imp C
5 3, 4 ax_mp 
A \imp B \imp C \iff A \and B \imp C

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)