Theorem nan

Description: Theorem to move a conjunct in and out of a negation. (Contributed by NM, 9-Nov-2003)

	Ref	Expression
Assertion	nan	|- ( ( ph -> -. ( ps /\ ch ) ) <-> ( ( ph /\ ps ) -> -. ch ) )

Proof

Step	Hyp	Ref	Expression
1		impexp	|- ( ( ( ph /\ ps ) -> -. ch ) <-> ( ph -> ( ps -> -. ch ) ) )
2		imnan	|- ( ( ps -> -. ch ) <-> -. ( ps /\ ch ) )
3	2	imbi2i	|- ( ( ph -> ( ps -> -. ch ) ) <-> ( ph -> -. ( ps /\ ch ) ) )
4	1 3	bitr2i	|- ( ( ph -> -. ( ps /\ ch ) ) <-> ( ( ph /\ ps ) -> -. ch ) )