Description: Triple conjunction expressed in terms of triple disjunction. (Contributed by Jeff Hankins, 15-Aug-2009) (Proof shortened by Wolf Lammen, 8-Apr-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 3anor | |- ( ( ph /\ ps /\ ch ) <-> -. ( -. ph \/ -. ps \/ -. ch ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 3ianor | |- ( -. ( ph /\ ps /\ ch ) <-> ( -. ph \/ -. ps \/ -. ch ) ) |
|
| 2 | 1 | con1bii | |- ( -. ( -. ph \/ -. ps \/ -. ch ) <-> ( ph /\ ps /\ ch ) ) |
| 3 | 2 | bicomi | |- ( ( ph /\ ps /\ ch ) <-> -. ( -. ph \/ -. ps \/ -. ch ) ) |