Description: Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | ifpnot23d | |- ( -. if- ( ph , -. ps , -. ch ) <-> if- ( ph , ps , ch ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ifpnot23 | |- ( -. if- ( ph , -. ps , -. ch ) <-> if- ( ph , -. -. ps , -. -. ch ) ) |
|
2 | notnotb | |- ( ps <-> -. -. ps ) |
|
3 | notnotb | |- ( ch <-> -. -. ch ) |
|
4 | ifpbi23 | |- ( ( ( ps <-> -. -. ps ) /\ ( ch <-> -. -. ch ) ) -> ( if- ( ph , ps , ch ) <-> if- ( ph , -. -. ps , -. -. ch ) ) ) |
|
5 | 2 3 4 | mp2an | |- ( if- ( ph , ps , ch ) <-> if- ( ph , -. -. ps , -. -. ch ) ) |
6 | 1 5 | bitr4i | |- ( -. if- ( ph , -. ps , -. ch ) <-> if- ( ph , ps , ch ) ) |