| Step |
Hyp |
Ref |
Expression |
| 1 |
|
3anass |
|- ( ( ph /\ ps /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) ) |
| 2 |
|
pm4.63 |
|- ( -. ( ps -> -. ch ) <-> ( ps /\ ch ) ) |
| 3 |
2
|
anbi2i |
|- ( ( ph /\ -. ( ps -> -. ch ) ) <-> ( ph /\ ( ps /\ ch ) ) ) |
| 4 |
|
annim |
|- ( ( ph /\ -. ( ps -> -. ch ) ) <-> -. ( ph -> ( ps -> -. ch ) ) ) |
| 5 |
1 3 4
|
3bitr2i |
|- ( ( ph /\ ps /\ ch ) <-> -. ( ph -> ( ps -> -. ch ) ) ) |
| 6 |
|
df-3nand |
|- ( ( ph -/\ ps -/\ ch ) <-> ( ph -> ( ps -> -. ch ) ) ) |
| 7 |
6
|
notbii |
|- ( -. ( ph -/\ ps -/\ ch ) <-> -. ( ph -> ( ps -> -. ch ) ) ) |
| 8 |
|
nannot |
|- ( -. ( ph -/\ ps -/\ ch ) <-> ( ( ph -/\ ps -/\ ch ) -/\ ( ph -/\ ps -/\ ch ) ) ) |
| 9 |
5 7 8
|
3bitr2i |
|- ( ( ph /\ ps /\ ch ) <-> ( ( ph -/\ ps -/\ ch ) -/\ ( ph -/\ ps -/\ ch ) ) ) |