Theorem imp_imp_perml ≪ | index | src | ≫

\imp对\imp左置换

theorem imp_imp_perml (A B C: wff): $ A \imp B \imp C \iff B \imp A \imp C $;
StepHypRefExpression
1 iff_comp 
((A \imp B \imp C) \imp B \imp A \imp C) \imp ((B \imp A \imp C) \imp A \imp B \imp C) \imp (A \imp B \imp C \iff B \imp A \imp C)
2 imp_imp_swapl 
(A \imp B \imp C) \imp B \imp A \imp C
3 1, 2 ax_mp 
((B \imp A \imp C) \imp A \imp B \imp C) \imp (A \imp B \imp C \iff B \imp A \imp C)
4 imp_imp_swapl 
(B \imp A \imp C) \imp A \imp B \imp C
5 3, 4 ax_mp 
A \imp B \imp C \iff B \imp A \imp C

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)