Metamath Proof Explorer

Theorem rblem4

Description: Used to rederive the Lukasiewicz axioms from Russell-Bernays'. (Contributed by Anthony Hart, 18-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses rblem4.1 
|- ( -. ph \/ th )
rblem4.2 
|- ( -. ps \/ ta )
rblem4.3 
|- ( -. ch \/ et )
Assertion rblem4 
|- ( -. ( ( ph \/ ps ) \/ ch ) \/ ( ( et \/ ta ) \/ th ) )

Proof

Step Hyp Ref Expression
1 rblem4.1 
 |-  ( -. ph \/ th )
2 rblem4.2 
 |-  ( -. ps \/ ta )
3 rblem4.3 
 |-  ( -. ch \/ et )
4 3 2 rblem1 
 |-  ( -. ( ch \/ ps ) \/ ( et \/ ta ) )
5 4 1 rblem1 
 |-  ( -. ( ( ch \/ ps ) \/ ph ) \/ ( ( et \/ ta ) \/ th ) )
6 rb-ax2 
 |-  ( -. ( ph \/ ( ch \/ ps ) ) \/ ( ( ch \/ ps ) \/ ph ) )
7 rb-ax2 
 |-  ( -. ( ps \/ ch ) \/ ( ch \/ ps ) )
8 rb-ax1 
 |-  ( -. ( -. ( ps \/ ch ) \/ ( ch \/ ps ) ) \/ ( -. ( ph \/ ( ps \/ ch ) ) \/ ( ph \/ ( ch \/ ps ) ) ) )
9 7 8 anmp 
 |-  ( -. ( ph \/ ( ps \/ ch ) ) \/ ( ph \/ ( ch \/ ps ) ) )
10 rb-ax2 
 |-  ( -. ( ( ps \/ ch ) \/ ph ) \/ ( ph \/ ( ps \/ ch ) ) )
11 9 10 rbsyl 
 |-  ( -. ( ( ps \/ ch ) \/ ph ) \/ ( ph \/ ( ch \/ ps ) ) )
12 6 11 rbsyl 
 |-  ( -. ( ( ps \/ ch ) \/ ph ) \/ ( ( ch \/ ps ) \/ ph ) )
13 rb-ax4 
 |-  ( -. ( ( ( ps \/ ch ) \/ ph ) \/ ( ( ps \/ ch ) \/ ph ) ) \/ ( ( ps \/ ch ) \/ ph ) )
14 rb-ax2 
 |-  ( -. ( ph \/ ( ps \/ ch ) ) \/ ( ( ps \/ ch ) \/ ph ) )
15 rblem2 
 |-  ( -. ( ph \/ ps ) \/ ( ph \/ ( ps \/ ch ) ) )
16 14 15 rbsyl 
 |-  ( -. ( ph \/ ps ) \/ ( ( ps \/ ch ) \/ ph ) )
17 rb-ax3 
 |-  ( -. ch \/ ( ps \/ ch ) )
18 rblem2 
 |-  ( -. ( -. ch \/ ( ps \/ ch ) ) \/ ( -. ch \/ ( ( ps \/ ch ) \/ ph ) ) )
19 17 18 anmp 
 |-  ( -. ch \/ ( ( ps \/ ch ) \/ ph ) )
20 16 19 rblem1 
 |-  ( -. ( ( ph \/ ps ) \/ ch ) \/ ( ( ( ps \/ ch ) \/ ph ) \/ ( ( ps \/ ch ) \/ ph ) ) )
21 13 20 rbsyl 
 |-  ( -. ( ( ph \/ ps ) \/ ch ) \/ ( ( ps \/ ch ) \/ ph ) )
22 12 21 rbsyl 
 |-  ( -. ( ( ph \/ ps ) \/ ch ) \/ ( ( ch \/ ps ) \/ ph ) )
23 5 22 rbsyl 
 |-  ( -. ( ( ph \/ ps ) \/ ch ) \/ ( ( et \/ ta ) \/ th ) )