Metamath Proof Explorer

Theorem re2luk1

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

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

Proof

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