Description: Disjunction distributes over the biconditional. An axiom of system DS in Vladimir Lifschitz, "On calculational proofs" (1998), http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.25.3384 . (Contributed by NM, 8-Jan-2005) (Proof shortened by Wolf Lammen, 4-Feb-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | orbidi | |- ( ( ph \/ ( ps <-> ch ) ) <-> ( ( ph \/ ps ) <-> ( ph \/ ch ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pm5.74 | |- ( ( -. ph -> ( ps <-> ch ) ) <-> ( ( -. ph -> ps ) <-> ( -. ph -> ch ) ) ) |
|
| 2 | df-or | |- ( ( ph \/ ( ps <-> ch ) ) <-> ( -. ph -> ( ps <-> ch ) ) ) |
|
| 3 | df-or | |- ( ( ph \/ ps ) <-> ( -. ph -> ps ) ) |
|
| 4 | df-or | |- ( ( ph \/ ch ) <-> ( -. ph -> ch ) ) |
|
| 5 | 3 4 | bibi12i | |- ( ( ( ph \/ ps ) <-> ( ph \/ ch ) ) <-> ( ( -. ph -> ps ) <-> ( -. ph -> ch ) ) ) |
| 6 | 1 2 5 | 3bitr4i | |- ( ( ph \/ ( ps <-> ch ) ) <-> ( ( ph \/ ps ) <-> ( ph \/ ch ) ) ) |