Description: Used to rederive the Lukasiewicz axioms from Russell-Bernays'. (Contributed by Anthony Hart, 19-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | rblem7.1 | |- -. ( -. ( -. ph \/ ps ) \/ -. ( -. ps \/ ph ) ) |
|
| Assertion | rblem7 | |- ( -. ps \/ ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rblem7.1 | |- -. ( -. ( -. ph \/ ps ) \/ -. ( -. ps \/ ph ) ) |
|
| 2 | rb-ax3 | |- ( -. -. ( -. ps \/ ph ) \/ ( -. ( -. ph \/ ps ) \/ -. ( -. ps \/ ph ) ) ) |
|
| 3 | rblem5 | |- ( -. ( -. -. ( -. ps \/ ph ) \/ ( -. ( -. ph \/ ps ) \/ -. ( -. ps \/ ph ) ) ) \/ ( -. -. ( -. ( -. ph \/ ps ) \/ -. ( -. ps \/ ph ) ) \/ ( -. ps \/ ph ) ) ) |
|
| 4 | 2 3 | anmp | |- ( -. -. ( -. ( -. ph \/ ps ) \/ -. ( -. ps \/ ph ) ) \/ ( -. ps \/ ph ) ) |
| 5 | 1 4 | anmp | |- ( -. ps \/ ph ) |