Theorem imp_repsecond ≪ | index | src | ≫

\imp替换第二位

theorem imp_repsecond (A B C D: wff):
  $ (A \imp B \imp C) \imp (D \imp B) \imp A \imp D \imp C $;
StepHypRefExpression
1 imp_imp_swapl 
((D \imp B) \imp (A \imp B \imp C) \imp A \imp D \imp C) \imp (A \imp B \imp C) \imp (D \imp B) \imp A \imp D \imp C
2 imp_tran 
((D \imp B) \imp (B \imp C) \imp D \imp C) \imp
  (((B \imp C) \imp D \imp C) \imp (A \imp B \imp C) \imp A \imp D \imp C) \imp
  (D \imp B) \imp
  (A \imp B \imp C) \imp
  A \imp
  D \imp
  C
3 imp_introrevr_imp 
(D \imp B) \imp (B \imp C) \imp D \imp C
4 2, 3 ax_mp 
(((B \imp C) \imp D \imp C) \imp (A \imp B \imp C) \imp A \imp D \imp C) \imp (D \imp B) \imp (A \imp B \imp C) \imp A \imp D \imp C
5 imp_introl_imp 
((B \imp C) \imp D \imp C) \imp (A \imp B \imp C) \imp A \imp D \imp C
6 4, 5 ax_mp 
(D \imp B) \imp (A \imp B \imp C) \imp A \imp D \imp C
7 1, 6 ax_mp 
(A \imp B \imp C) \imp (D \imp B) \imp A \imp D \imp C

Axiom use

Logic (ax_mp, ax_1, ax_2)