Description: A Tseitin axiom for logical biconditional, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | tsbi4 | |- ( th -> ( ( -. ph \/ ps ) \/ -. ( ph <-> ps ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tsbi3 | |- ( th -> ( ( ps \/ -. ph ) \/ -. ( ps <-> ph ) ) ) |
|
2 | orcom | |- ( ( ps \/ -. ph ) <-> ( -. ph \/ ps ) ) |
|
3 | bicom | |- ( ( ps <-> ph ) <-> ( ph <-> ps ) ) |
|
4 | 3 | notbii | |- ( -. ( ps <-> ph ) <-> -. ( ph <-> ps ) ) |
5 | 2 4 | orbi12i | |- ( ( ( ps \/ -. ph ) \/ -. ( ps <-> ph ) ) <-> ( ( -. ph \/ ps ) \/ -. ( ph <-> ps ) ) ) |
6 | 1 5 | sylib | |- ( th -> ( ( -. ph \/ ps ) \/ -. ( ph <-> ps ) ) ) |