Theorem re2luk1 1773

Description: luk-1 1663 derived from Russell-Bernays'. (Contributed by Anthony Hart, 19-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
re2luk1	⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))

Proof of Theorem re2luk1

Step	Hyp	Ref	Expression
1		rb-imdf 1758	. . . 4 ⊢ ¬ (¬ (¬ ((𝜓 → 𝜒) → (𝜑 → 𝜒)) ∨ (¬ (𝜓 → 𝜒) ∨ (𝜑 → 𝜒))) ∨ ¬ (¬ (¬ (𝜓 → 𝜒) ∨ (𝜑 → 𝜒)) ∨ ((𝜓 → 𝜒) → (𝜑 → 𝜒))))
2	1	rblem7 1771	. . 3 ⊢ (¬ (¬ (𝜓 → 𝜒) ∨ (𝜑 → 𝜒)) ∨ ((𝜓 → 𝜒) → (𝜑 → 𝜒)))
3		rb-imdf 1758	. . . . . . . 8 ⊢ ¬ (¬ (¬ (𝜓 → 𝜒) ∨ (¬ 𝜓 ∨ 𝜒)) ∨ ¬ (¬ (¬ 𝜓 ∨ 𝜒) ∨ (𝜓 → 𝜒)))
4	3	rblem6 1770	. . . . . . 7 ⊢ (¬ (𝜓 → 𝜒) ∨ (¬ 𝜓 ∨ 𝜒))
5		rb-ax2 1761	. . . . . . . 8 ⊢ (¬ (¬ (𝜓 → 𝜒) ∨ ¬ ¬ (¬ 𝜓 ∨ 𝜒)) ∨ (¬ ¬ (¬ 𝜓 ∨ 𝜒) ∨ ¬ (𝜓 → 𝜒)))
6		rb-ax4 1763	. . . . . . . . . 10 ⊢ (¬ (¬ (𝜓 → 𝜒) ∨ ¬ (𝜓 → 𝜒)) ∨ ¬ (𝜓 → 𝜒))
7		rb-ax3 1762	. . . . . . . . . 10 ⊢ (¬ ¬ (𝜓 → 𝜒) ∨ (¬ (𝜓 → 𝜒) ∨ ¬ (𝜓 → 𝜒)))
8	6, 7	rbsyl 1764	. . . . . . . . 9 ⊢ (¬ ¬ (𝜓 → 𝜒) ∨ ¬ (𝜓 → 𝜒))
9		rb-ax4 1763	. . . . . . . . . . 11 ⊢ (¬ (¬ (¬ 𝜓 ∨ 𝜒) ∨ ¬ (¬ 𝜓 ∨ 𝜒)) ∨ ¬ (¬ 𝜓 ∨ 𝜒))
10		rb-ax3 1762	. . . . . . . . . . 11 ⊢ (¬ ¬ (¬ 𝜓 ∨ 𝜒) ∨ (¬ (¬ 𝜓 ∨ 𝜒) ∨ ¬ (¬ 𝜓 ∨ 𝜒)))
11	9, 10	rbsyl 1764	. . . . . . . . . 10 ⊢ (¬ ¬ (¬ 𝜓 ∨ 𝜒) ∨ ¬ (¬ 𝜓 ∨ 𝜒))
12		rb-ax2 1761	. . . . . . . . . 10 ⊢ (¬ (¬ ¬ (¬ 𝜓 ∨ 𝜒) ∨ ¬ (¬ 𝜓 ∨ 𝜒)) ∨ (¬ (¬ 𝜓 ∨ 𝜒) ∨ ¬ ¬ (¬ 𝜓 ∨ 𝜒)))
13	11, 12	anmp 1759	. . . . . . . . 9 ⊢ (¬ (¬ 𝜓 ∨ 𝜒) ∨ ¬ ¬ (¬ 𝜓 ∨ 𝜒))
14	8, 13	rblem1 1765	. . . . . . . 8 ⊢ (¬ (¬ (𝜓 → 𝜒) ∨ (¬ 𝜓 ∨ 𝜒)) ∨ (¬ (𝜓 → 𝜒) ∨ ¬ ¬ (¬ 𝜓 ∨ 𝜒)))
15	5, 14	rbsyl 1764	. . . . . . 7 ⊢ (¬ (¬ (𝜓 → 𝜒) ∨ (¬ 𝜓 ∨ 𝜒)) ∨ (¬ ¬ (¬ 𝜓 ∨ 𝜒) ∨ ¬ (𝜓 → 𝜒)))
16	4, 15	anmp 1759	. . . . . 6 ⊢ (¬ ¬ (¬ 𝜓 ∨ 𝜒) ∨ ¬ (𝜓 → 𝜒))
17		rb-imdf 1758	. . . . . . 7 ⊢ ¬ (¬ (¬ (𝜑 → 𝜒) ∨ (¬ 𝜑 ∨ 𝜒)) ∨ ¬ (¬ (¬ 𝜑 ∨ 𝜒) ∨ (𝜑 → 𝜒)))
18	17	rblem7 1771	. . . . . 6 ⊢ (¬ (¬ 𝜑 ∨ 𝜒) ∨ (𝜑 → 𝜒))
19	16, 18	rblem1 1765	. . . . 5 ⊢ (¬ (¬ (¬ 𝜓 ∨ 𝜒) ∨ (¬ 𝜑 ∨ 𝜒)) ∨ (¬ (𝜓 → 𝜒) ∨ (𝜑 → 𝜒)))
20		rb-ax1 1760	. . . . . 6 ⊢ (¬ (¬ 𝜓 ∨ 𝜒) ∨ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (¬ 𝜑 ∨ 𝜒)))
21		rb-ax2 1761	. . . . . . 7 ⊢ (¬ ((¬ (¬ 𝜓 ∨ 𝜒) ∨ (¬ 𝜑 ∨ 𝜒)) ∨ ¬ (¬ 𝜑 ∨ 𝜓)) ∨ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (¬ (¬ 𝜓 ∨ 𝜒) ∨ (¬ 𝜑 ∨ 𝜒))))
22		rb-ax4 1763	. . . . . . . . . 10 ⊢ (¬ (¬ (¬ 𝜑 ∨ 𝜓) ∨ ¬ (¬ 𝜑 ∨ 𝜓)) ∨ ¬ (¬ 𝜑 ∨ 𝜓))
23		rb-ax3 1762	. . . . . . . . . 10 ⊢ (¬ ¬ (¬ 𝜑 ∨ 𝜓) ∨ (¬ (¬ 𝜑 ∨ 𝜓) ∨ ¬ (¬ 𝜑 ∨ 𝜓)))
24	22, 23	rbsyl 1764	. . . . . . . . 9 ⊢ (¬ ¬ (¬ 𝜑 ∨ 𝜓) ∨ ¬ (¬ 𝜑 ∨ 𝜓))
25		rb-ax4 1763	. . . . . . . . . 10 ⊢ (¬ ((¬ 𝜑 ∨ 𝜒) ∨ (¬ 𝜑 ∨ 𝜒)) ∨ (¬ 𝜑 ∨ 𝜒))
26		rb-ax3 1762	. . . . . . . . . 10 ⊢ (¬ (¬ 𝜑 ∨ 𝜒) ∨ ((¬ 𝜑 ∨ 𝜒) ∨ (¬ 𝜑 ∨ 𝜒)))
27	25, 26	rbsyl 1764	. . . . . . . . 9 ⊢ (¬ (¬ 𝜑 ∨ 𝜒) ∨ (¬ 𝜑 ∨ 𝜒))
28	24, 27, 11	rblem4 1768	. . . . . . . 8 ⊢ (¬ ((¬ (¬ 𝜑 ∨ 𝜓) ∨ (¬ 𝜑 ∨ 𝜒)) ∨ ¬ (¬ 𝜓 ∨ 𝜒)) ∨ ((¬ (¬ 𝜓 ∨ 𝜒) ∨ (¬ 𝜑 ∨ 𝜒)) ∨ ¬ (¬ 𝜑 ∨ 𝜓)))
29		rb-ax2 1761	. . . . . . . 8 ⊢ (¬ (¬ (¬ 𝜓 ∨ 𝜒) ∨ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (¬ 𝜑 ∨ 𝜒))) ∨ ((¬ (¬ 𝜑 ∨ 𝜓) ∨ (¬ 𝜑 ∨ 𝜒)) ∨ ¬ (¬ 𝜓 ∨ 𝜒)))
30	28, 29	rbsyl 1764	. . . . . . 7 ⊢ (¬ (¬ (¬ 𝜓 ∨ 𝜒) ∨ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (¬ 𝜑 ∨ 𝜒))) ∨ ((¬ (¬ 𝜓 ∨ 𝜒) ∨ (¬ 𝜑 ∨ 𝜒)) ∨ ¬ (¬ 𝜑 ∨ 𝜓)))
31	21, 30	rbsyl 1764	. . . . . 6 ⊢ (¬ (¬ (¬ 𝜓 ∨ 𝜒) ∨ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (¬ 𝜑 ∨ 𝜒))) ∨ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (¬ (¬ 𝜓 ∨ 𝜒) ∨ (¬ 𝜑 ∨ 𝜒))))
32	20, 31	anmp 1759	. . . . 5 ⊢ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (¬ (¬ 𝜓 ∨ 𝜒) ∨ (¬ 𝜑 ∨ 𝜒)))
33	19, 32	rbsyl 1764	. . . 4 ⊢ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (¬ (𝜓 → 𝜒) ∨ (𝜑 → 𝜒)))
34		rb-imdf 1758	. . . . 5 ⊢ ¬ (¬ (¬ (𝜑 → 𝜓) ∨ (¬ 𝜑 ∨ 𝜓)) ∨ ¬ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (𝜑 → 𝜓)))
35	34	rblem6 1770	. . . 4 ⊢ (¬ (𝜑 → 𝜓) ∨ (¬ 𝜑 ∨ 𝜓))
36	33, 35	rbsyl 1764	. . 3 ⊢ (¬ (𝜑 → 𝜓) ∨ (¬ (𝜓 → 𝜒) ∨ (𝜑 → 𝜒)))
37	2, 36	rbsyl 1764	. 2 ⊢ (¬ (𝜑 → 𝜓) ∨ ((𝜓 → 𝜒) → (𝜑 → 𝜒)))
38		rb-imdf 1758	. . 3 ⊢ ¬ (¬ (¬ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒))) ∨ (¬ (𝜑 → 𝜓) ∨ ((𝜓 → 𝜒) → (𝜑 → 𝜒)))) ∨ ¬ (¬ (¬ (𝜑 → 𝜓) ∨ ((𝜓 → 𝜒) → (𝜑 → 𝜒))) ∨ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))))
39	38	rblem7 1771	. 2 ⊢ (¬ (¬ (𝜑 → 𝜓) ∨ ((𝜓 → 𝜒) → (𝜑 → 𝜒))) ∨ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒))))
40	37, 39	anmp 1759	1 ⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 847

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848

This theorem is referenced by: (None)