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 
|- ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) )

Proof

Step Hyp Ref Expression
1 rb-imdf 
 |-  -. ( -. ( -. ( ( ps -> ch ) -> ( ph -> ch ) ) \/ ( -. ( ps -> ch ) \/ ( ph -> ch ) ) ) \/ -. ( -. ( -. ( ps -> ch ) \/ ( ph -> ch ) ) \/ ( ( ps -> ch ) -> ( ph -> ch ) ) ) )
2 1 rblem7 
 |-  ( -. ( -. ( ps -> ch ) \/ ( ph -> ch ) ) \/ ( ( ps -> ch ) -> ( ph -> ch ) ) )
3 rb-imdf 
 |-  -. ( -. ( -. ( ps -> ch ) \/ ( -. ps \/ ch ) ) \/ -. ( -. ( -. ps \/ ch ) \/ ( ps -> ch ) ) )
4 3 rblem6 
 |-  ( -. ( ps -> ch ) \/ ( -. ps \/ ch ) )
5 rb-ax2 
 |-  ( -. ( -. ( ps -> ch ) \/ -. -. ( -. ps \/ ch ) ) \/ ( -. -. ( -. ps \/ ch ) \/ -. ( ps -> ch ) ) )
6 rb-ax4 
 |-  ( -. ( -. ( ps -> ch ) \/ -. ( ps -> ch ) ) \/ -. ( ps -> ch ) )
7 rb-ax3 
 |-  ( -. -. ( ps -> ch ) \/ ( -. ( ps -> ch ) \/ -. ( ps -> ch ) ) )
8 6 7 rbsyl 
 |-  ( -. -. ( ps -> ch ) \/ -. ( ps -> ch ) )
9 rb-ax4 
 |-  ( -. ( -. ( -. ps \/ ch ) \/ -. ( -. ps \/ ch ) ) \/ -. ( -. ps \/ ch ) )
10 rb-ax3 
 |-  ( -. -. ( -. ps \/ ch ) \/ ( -. ( -. ps \/ ch ) \/ -. ( -. ps \/ ch ) ) )
11 9 10 rbsyl 
 |-  ( -. -. ( -. ps \/ ch ) \/ -. ( -. ps \/ ch ) )
12 rb-ax2 
 |-  ( -. ( -. -. ( -. ps \/ ch ) \/ -. ( -. ps \/ ch ) ) \/ ( -. ( -. ps \/ ch ) \/ -. -. ( -. ps \/ ch ) ) )
13 11 12 anmp 
 |-  ( -. ( -. ps \/ ch ) \/ -. -. ( -. ps \/ ch ) )
14 8 13 rblem1 
 |-  ( -. ( -. ( ps -> ch ) \/ ( -. ps \/ ch ) ) \/ ( -. ( ps -> ch ) \/ -. -. ( -. ps \/ ch ) ) )
15 5 14 rbsyl 
 |-  ( -. ( -. ( ps -> ch ) \/ ( -. ps \/ ch ) ) \/ ( -. -. ( -. ps \/ ch ) \/ -. ( ps -> ch ) ) )
16 4 15 anmp 
 |-  ( -. -. ( -. ps \/ ch ) \/ -. ( ps -> ch ) )
17 rb-imdf 
 |-  -. ( -. ( -. ( ph -> ch ) \/ ( -. ph \/ ch ) ) \/ -. ( -. ( -. ph \/ ch ) \/ ( ph -> ch ) ) )
18 17 rblem7 
 |-  ( -. ( -. ph \/ ch ) \/ ( ph -> ch ) )
19 16 18 rblem1 
 |-  ( -. ( -. ( -. ps \/ ch ) \/ ( -. ph \/ ch ) ) \/ ( -. ( ps -> ch ) \/ ( ph -> ch ) ) )
20 rb-ax1 
 |-  ( -. ( -. ps \/ ch ) \/ ( -. ( -. ph \/ ps ) \/ ( -. ph \/ ch ) ) )
21 rb-ax2 
 |-  ( -. ( ( -. ( -. ps \/ ch ) \/ ( -. ph \/ ch ) ) \/ -. ( -. ph \/ ps ) ) \/ ( -. ( -. ph \/ ps ) \/ ( -. ( -. ps \/ ch ) \/ ( -. ph \/ ch ) ) ) )
22 rb-ax4 
 |-  ( -. ( -. ( -. ph \/ ps ) \/ -. ( -. ph \/ ps ) ) \/ -. ( -. ph \/ ps ) )
23 rb-ax3 
 |-  ( -. -. ( -. ph \/ ps ) \/ ( -. ( -. ph \/ ps ) \/ -. ( -. ph \/ ps ) ) )
24 22 23 rbsyl 
 |-  ( -. -. ( -. ph \/ ps ) \/ -. ( -. ph \/ ps ) )
25 rb-ax4 
 |-  ( -. ( ( -. ph \/ ch ) \/ ( -. ph \/ ch ) ) \/ ( -. ph \/ ch ) )
26 rb-ax3 
 |-  ( -. ( -. ph \/ ch ) \/ ( ( -. ph \/ ch ) \/ ( -. ph \/ ch ) ) )
27 25 26 rbsyl 
 |-  ( -. ( -. ph \/ ch ) \/ ( -. ph \/ ch ) )
28 24 27 11 rblem4 
 |-  ( -. ( ( -. ( -. ph \/ ps ) \/ ( -. ph \/ ch ) ) \/ -. ( -. ps \/ ch ) ) \/ ( ( -. ( -. ps \/ ch ) \/ ( -. ph \/ ch ) ) \/ -. ( -. ph \/ ps ) ) )
29 rb-ax2 
 |-  ( -. ( -. ( -. ps \/ ch ) \/ ( -. ( -. ph \/ ps ) \/ ( -. ph \/ ch ) ) ) \/ ( ( -. ( -. ph \/ ps ) \/ ( -. ph \/ ch ) ) \/ -. ( -. ps \/ ch ) ) )
30 28 29 rbsyl 
 |-  ( -. ( -. ( -. ps \/ ch ) \/ ( -. ( -. ph \/ ps ) \/ ( -. ph \/ ch ) ) ) \/ ( ( -. ( -. ps \/ ch ) \/ ( -. ph \/ ch ) ) \/ -. ( -. ph \/ ps ) ) )
31 21 30 rbsyl 
 |-  ( -. ( -. ( -. ps \/ ch ) \/ ( -. ( -. ph \/ ps ) \/ ( -. ph \/ ch ) ) ) \/ ( -. ( -. ph \/ ps ) \/ ( -. ( -. ps \/ ch ) \/ ( -. ph \/ ch ) ) ) )
32 20 31 anmp 
 |-  ( -. ( -. ph \/ ps ) \/ ( -. ( -. ps \/ ch ) \/ ( -. ph \/ ch ) ) )
33 19 32 rbsyl 
 |-  ( -. ( -. ph \/ ps ) \/ ( -. ( ps -> ch ) \/ ( ph -> ch ) ) )
34 rb-imdf 
 |-  -. ( -. ( -. ( ph -> ps ) \/ ( -. ph \/ ps ) ) \/ -. ( -. ( -. ph \/ ps ) \/ ( ph -> ps ) ) )
35 34 rblem6 
 |-  ( -. ( ph -> ps ) \/ ( -. ph \/ ps ) )
36 33 35 rbsyl 
 |-  ( -. ( ph -> ps ) \/ ( -. ( ps -> ch ) \/ ( ph -> ch ) ) )
37 2 36 rbsyl 
 |-  ( -. ( ph -> ps ) \/ ( ( ps -> ch ) -> ( ph -> ch ) ) )
38 rb-imdf 
 |-  -. ( -. ( -. ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) \/ ( -. ( ph -> ps ) \/ ( ( ps -> ch ) -> ( ph -> ch ) ) ) ) \/ -. ( -. ( -. ( ph -> ps ) \/ ( ( ps -> ch ) -> ( ph -> ch ) ) ) \/ ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) ) )
39 38 rblem7 
 |-  ( -. ( -. ( ph -> ps ) \/ ( ( ps -> ch ) -> ( ph -> ch ) ) ) \/ ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) )
40 37 39 anmp 
 |-  ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) )