Description: Distributive law for disjunction. Theorem *4.41 of WhiteheadRussell p. 119. (Contributed by NM, 5-Jan-1993) (Proof shortened by Andrew Salmon, 7-May-2011) (Proof shortened by Wolf Lammen, 28-Nov-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ordi | |- ( ( ph \/ ( ps /\ ch ) ) <-> ( ( ph \/ ps ) /\ ( ph \/ ch ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | jcab | |- ( ( -. 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 | anbi12i | |- ( ( ( ph \/ ps ) /\ ( ph \/ ch ) ) <-> ( ( -. ph -> ps ) /\ ( -. ph -> ch ) ) ) |
| 6 | 1 2 5 | 3bitr4i | |- ( ( ph \/ ( ps /\ ch ) ) <-> ( ( ph \/ ps ) /\ ( ph \/ ch ) ) ) |