Description: A conjunction with a negated conjunction. (Contributed by AV, 8-Mar-2022) (Proof shortened by Wolf Lammen, 1-Apr-2022)
Ref | Expression | ||
---|---|---|---|
Assertion | annotanannot | |- ( ( ph /\ -. ( ph /\ ps ) ) <-> ( ph /\ -. ps ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ibar | |- ( ph -> ( ps <-> ( ph /\ ps ) ) ) |
|
2 | 1 | bicomd | |- ( ph -> ( ( ph /\ ps ) <-> ps ) ) |
3 | 2 | notbid | |- ( ph -> ( -. ( ph /\ ps ) <-> -. ps ) ) |
4 | 3 | pm5.32i | |- ( ( ph /\ -. ( ph /\ ps ) ) <-> ( ph /\ -. ps ) ) |