Theorem imp_for_imp_left_permute ≪ | index | src | ≫

→对→左置换

theorem imp_for_imp_left_permute (A B C: wff):
  $ (A \imp B \imp C) \imp B \imp A \imp C $;
StepHypRefExpression
1 imp_for_imp_left_intro 
((B \imp A \imp B \imp C) \imp B \imp A \imp C) \imp ((A \imp B \imp C) \imp B \imp A \imp B \imp C) \imp (A \imp B \imp C) \imp B \imp A \imp C
2 imp_for_imp_left_insert 
(B \imp (A \imp B \imp C) \imp A \imp C) \imp (B \imp A \imp B \imp C) \imp B \imp A \imp C
3 imp_for_imp_left_intro 
((A \imp B) \imp (A \imp B \imp C) \imp A \imp C) \imp (B \imp A \imp B) \imp B \imp (A \imp B \imp C) \imp A \imp C
4 imp_for_imp_left_intro 
(((A \imp B \imp C) \imp A \imp B) \imp (A \imp B \imp C) \imp A \imp C) \imp
  ((A \imp B) \imp (A \imp B \imp C) \imp A \imp B) \imp
  (A \imp B) \imp
  (A \imp B \imp C) \imp
  A \imp
  C
5 imp_for_imp_left_insert 
((A \imp B \imp C) \imp (A \imp B) \imp A \imp C) \imp ((A \imp B \imp C) \imp A \imp B) \imp (A \imp B \imp C) \imp A \imp C
6 imp_for_imp_left_insert 
(A \imp B \imp C) \imp (A \imp B) \imp A \imp C
7 5, 6 mp 
((A \imp B \imp C) \imp A \imp B) \imp (A \imp B \imp C) \imp A \imp C
8 4, 7 mp 
((A \imp B) \imp (A \imp B \imp C) \imp A \imp B) \imp (A \imp B) \imp (A \imp B \imp C) \imp A \imp C
9 imp_left_intro 
(A \imp B) \imp (A \imp B \imp C) \imp A \imp B
10 8, 9 mp 
(A \imp B) \imp (A \imp B \imp C) \imp A \imp C
11 3, 10 mp 
(B \imp A \imp B) \imp B \imp (A \imp B \imp C) \imp A \imp C
12 imp_left_intro 
B \imp A \imp B
13 11, 12 mp 
B \imp (A \imp B \imp C) \imp A \imp C
14 2, 13 mp 
(B \imp A \imp B \imp C) \imp B \imp A \imp C
15 1, 14 mp 
((A \imp B \imp C) \imp B \imp A \imp B \imp C) \imp (A \imp B \imp C) \imp B \imp A \imp C
16 imp_left_intro 
(A \imp B \imp C) \imp B \imp A \imp B \imp C
17 15, 16 mp 
(A \imp B \imp C) \imp B \imp A \imp C

Axiom use

ZFC (ax_mp, ax_p1, ax_p2)