Theorem re2luk1 1530

Description: luk-1 1420 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 1515	. . . 4 ⊢ ¬ (¬ (¬ ((ψ → χ) → (φ → χ)) ∨ (¬ (ψ → χ) ∨ (φ → χ))) ∨ ¬ (¬ (¬ (ψ → χ) ∨ (φ → χ)) ∨ ((ψ → χ) → (φ → χ))))
2	1	rblem7 1528	. . 3 ⊢ (¬ (¬ (ψ → χ) ∨ (φ → χ)) ∨ ((ψ → χ) → (φ → χ)))
3		rb-imdf 1515	. . . . . . . 8 ⊢ ¬ (¬ (¬ (ψ → χ) ∨ (¬ ψ ∨ χ)) ∨ ¬ (¬ (¬ ψ ∨ χ) ∨ (ψ → χ)))
4	3	rblem6 1527	. . . . . . 7 ⊢ (¬ (ψ → χ) ∨ (¬ ψ ∨ χ))
5		rb-ax2 1518	. . . . . . . 8 ⊢ (¬ (¬ (ψ → χ) ∨ ¬ ¬ (¬ ψ ∨ χ)) ∨ (¬ ¬ (¬ ψ ∨ χ) ∨ ¬ (ψ → χ)))
6		rb-ax4 1520	. . . . . . . . . 10 ⊢ (¬ (¬ (ψ → χ) ∨ ¬ (ψ → χ)) ∨ ¬ (ψ → χ))
7		rb-ax3 1519	. . . . . . . . . 10 ⊢ (¬ ¬ (ψ → χ) ∨ (¬ (ψ → χ) ∨ ¬ (ψ → χ)))
8	6, 7	rbsyl 1521	. . . . . . . . 9 ⊢ (¬ ¬ (ψ → χ) ∨ ¬ (ψ → χ))
9		rb-ax4 1520	. . . . . . . . . . 11 ⊢ (¬ (¬ (¬ ψ ∨ χ) ∨ ¬ (¬ ψ ∨ χ)) ∨ ¬ (¬ ψ ∨ χ))
10		rb-ax3 1519	. . . . . . . . . . 11 ⊢ (¬ ¬ (¬ ψ ∨ χ) ∨ (¬ (¬ ψ ∨ χ) ∨ ¬ (¬ ψ ∨ χ)))
11	9, 10	rbsyl 1521	. . . . . . . . . 10 ⊢ (¬ ¬ (¬ ψ ∨ χ) ∨ ¬ (¬ ψ ∨ χ))
12		rb-ax2 1518	. . . . . . . . . 10 ⊢ (¬ (¬ ¬ (¬ ψ ∨ χ) ∨ ¬ (¬ ψ ∨ χ)) ∨ (¬ (¬ ψ ∨ χ) ∨ ¬ ¬ (¬ ψ ∨ χ)))
13	11, 12	anmp 1516	. . . . . . . . 9 ⊢ (¬ (¬ ψ ∨ χ) ∨ ¬ ¬ (¬ ψ ∨ χ))
14	8, 13	rblem1 1522	. . . . . . . 8 ⊢ (¬ (¬ (ψ → χ) ∨ (¬ ψ ∨ χ)) ∨ (¬ (ψ → χ) ∨ ¬ ¬ (¬ ψ ∨ χ)))
15	5, 14	rbsyl 1521	. . . . . . 7 ⊢ (¬ (¬ (ψ → χ) ∨ (¬ ψ ∨ χ)) ∨ (¬ ¬ (¬ ψ ∨ χ) ∨ ¬ (ψ → χ)))
16	4, 15	anmp 1516	. . . . . 6 ⊢ (¬ ¬ (¬ ψ ∨ χ) ∨ ¬ (ψ → χ))
17		rb-imdf 1515	. . . . . . 7 ⊢ ¬ (¬ (¬ (φ → χ) ∨ (¬ φ ∨ χ)) ∨ ¬ (¬ (¬ φ ∨ χ) ∨ (φ → χ)))
18	17	rblem7 1528	. . . . . 6 ⊢ (¬ (¬ φ ∨ χ) ∨ (φ → χ))
19	16, 18	rblem1 1522	. . . . 5 ⊢ (¬ (¬ (¬ ψ ∨ χ) ∨ (¬ φ ∨ χ)) ∨ (¬ (ψ → χ) ∨ (φ → χ)))
20		rb-ax1 1517	. . . . . 6 ⊢ (¬ (¬ ψ ∨ χ) ∨ (¬ (¬ φ ∨ ψ) ∨ (¬ φ ∨ χ)))
21		rb-ax2 1518	. . . . . . 7 ⊢ (¬ ((¬ (¬ ψ ∨ χ) ∨ (¬ φ ∨ χ)) ∨ ¬ (¬ φ ∨ ψ)) ∨ (¬ (¬ φ ∨ ψ) ∨ (¬ (¬ ψ ∨ χ) ∨ (¬ φ ∨ χ))))
22		rb-ax4 1520	. . . . . . . . . 10 ⊢ (¬ (¬ (¬ φ ∨ ψ) ∨ ¬ (¬ φ ∨ ψ)) ∨ ¬ (¬ φ ∨ ψ))
23		rb-ax3 1519	. . . . . . . . . 10 ⊢ (¬ ¬ (¬ φ ∨ ψ) ∨ (¬ (¬ φ ∨ ψ) ∨ ¬ (¬ φ ∨ ψ)))
24	22, 23	rbsyl 1521	. . . . . . . . 9 ⊢ (¬ ¬ (¬ φ ∨ ψ) ∨ ¬ (¬ φ ∨ ψ))
25		rb-ax4 1520	. . . . . . . . . 10 ⊢ (¬ ((¬ φ ∨ χ) ∨ (¬ φ ∨ χ)) ∨ (¬ φ ∨ χ))
26		rb-ax3 1519	. . . . . . . . . 10 ⊢ (¬ (¬ φ ∨ χ) ∨ ((¬ φ ∨ χ) ∨ (¬ φ ∨ χ)))
27	25, 26	rbsyl 1521	. . . . . . . . 9 ⊢ (¬ (¬ φ ∨ χ) ∨ (¬ φ ∨ χ))
28	24, 27, 11	rblem4 1525	. . . . . . . 8 ⊢ (¬ ((¬ (¬ φ ∨ ψ) ∨ (¬ φ ∨ χ)) ∨ ¬ (¬ ψ ∨ χ)) ∨ ((¬ (¬ ψ ∨ χ) ∨ (¬ φ ∨ χ)) ∨ ¬ (¬ φ ∨ ψ)))
29		rb-ax2 1518	. . . . . . . 8 ⊢ (¬ (¬ (¬ ψ ∨ χ) ∨ (¬ (¬ φ ∨ ψ) ∨ (¬ φ ∨ χ))) ∨ ((¬ (¬ φ ∨ ψ) ∨ (¬ φ ∨ χ)) ∨ ¬ (¬ ψ ∨ χ)))
30	28, 29	rbsyl 1521	. . . . . . 7 ⊢ (¬ (¬ (¬ ψ ∨ χ) ∨ (¬ (¬ φ ∨ ψ) ∨ (¬ φ ∨ χ))) ∨ ((¬ (¬ ψ ∨ χ) ∨ (¬ φ ∨ χ)) ∨ ¬ (¬ φ ∨ ψ)))
31	21, 30	rbsyl 1521	. . . . . 6 ⊢ (¬ (¬ (¬ ψ ∨ χ) ∨ (¬ (¬ φ ∨ ψ) ∨ (¬ φ ∨ χ))) ∨ (¬ (¬ φ ∨ ψ) ∨ (¬ (¬ ψ ∨ χ) ∨ (¬ φ ∨ χ))))
32	20, 31	anmp 1516	. . . . 5 ⊢ (¬ (¬ φ ∨ ψ) ∨ (¬ (¬ ψ ∨ χ) ∨ (¬ φ ∨ χ)))
33	19, 32	rbsyl 1521	. . . 4 ⊢ (¬ (¬ φ ∨ ψ) ∨ (¬ (ψ → χ) ∨ (φ → χ)))
34		rb-imdf 1515	. . . . 5 ⊢ ¬ (¬ (¬ (φ → ψ) ∨ (¬ φ ∨ ψ)) ∨ ¬ (¬ (¬ φ ∨ ψ) ∨ (φ → ψ)))
35	34	rblem6 1527	. . . 4 ⊢ (¬ (φ → ψ) ∨ (¬ φ ∨ ψ))
36	33, 35	rbsyl 1521	. . 3 ⊢ (¬ (φ → ψ) ∨ (¬ (ψ → χ) ∨ (φ → χ)))
37	2, 36	rbsyl 1521	. 2 ⊢ (¬ (φ → ψ) ∨ ((ψ → χ) → (φ → χ)))
38		rb-imdf 1515	. . 3 ⊢ ¬ (¬ (¬ ((φ → ψ) → ((ψ → χ) → (φ → χ))) ∨ (¬ (φ → ψ) ∨ ((ψ → χ) → (φ → χ)))) ∨ ¬ (¬ (¬ (φ → ψ) ∨ ((ψ → χ) → (φ → χ))) ∨ ((φ → ψ) → ((ψ → χ) → (φ → χ)))))
39	38	rblem7 1528	. 2 ⊢ (¬ (¬ (φ → ψ) ∨ ((ψ → χ) → (φ → χ))) ∨ ((φ → ψ) → ((ψ → χ) → (φ → χ))))
40	37, 39	anmp 1516	1 ⊢ ((φ → ψ) → ((ψ → χ) → (φ → χ)))

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

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 177  df-or 359  df-an 360

This theorem is referenced by: (None)